Theorem pm3.2 305

Description: Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111.

Assertion

Ref	Expression
pm3.2	|- (ph -> (ps -> (ph /\ ps)))

Proof of Theorem pm3.2

Step	Hyp	Ref	Expression
1		df-an 242	. . 3 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	biimpri 169	. 2 |- (-. (ph -> -. ps) -> (ph /\ ps))
3	2	expi 161	1 |- (ph -> (ps -> (ph /\ ps)))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240

This theorem is referenced by:  pm3.21 306  pm3.2i 307  pm3.43i 309  ancl 318  anc2l 324  anidm 478  prth 615  pm3.2an3 1049  19.26 1416  19.29 1421  r19.26 2219  r19.29 2227  difrab 2868  opelopab2 3569  dmcosseq 4214  fvopab6 4757  tratrb 5831  lediv2a 7080  2climnn 8362  2climnn0 8363  climserzlei 8407  alephexp2 8855  cnpco 9046  bnj1170 12962  axextndbi 13871  soxp 13950  and4as 14266  nxtand 14313  prjmapcp2 14515  iscnp3 14946  phtpcdm 16061  isdivrng3 16112  pm5.31r 16240  pm11.71 16354  elex22VD 16663  en3lplem1VD 16667  tratrbVD 16685  undif3VD 16706

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain