Theorem pm3.2 281

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 223	. . 3 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	biimpri 150	. 2 |- (-. (ph -> -. ps) -> (ph /\ ps))
3	2	expi 142	1 |- (ph -> (ps -> (ph /\ ps)))

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

This theorem is referenced by:  pm3.21 282  pm3.2i 283  pm3.43i 285  ancl 292  anc2l 298  anidm 433  prth 559  19.26 1103  difrab 2325  opelopab2 2896  fvopab6 3905  indpi 5188  lediv2a 6042  2climnn 7305  2climnn0 7306  climserzlei 7350  alephexp2 7798  cnpco 7979  and4as 10716  and4com 10717  phtpcdm 12103

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 145  df-an 223

Copyright terms: Public domain