Theorem pm3.2 283

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 225	. . 3 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2	1	biimpr 152	. 2 |- (-. (ph -> -. ps) -> (ph /\ ps))
3	2	expi 144	1 |- (ph -> (ps -> (ph /\ ps)))

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

This theorem is referenced by:  pm3.21 284  pm3.2i 285  pm3.43i 287  ancl 294  anc2l 300  anidm 432  prth 554  19.26 1063  difrab 2263  opelopab2 2808  indpi 5006  lemulge11t 5804  lediv2it 5845  2climnn 7039  2climnn0 7040  climserzle 7083  alephexp2 7528  cnpco 7708  and4as 10332  and4com 10333

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 147  df-an 225

Copyright terms: Public domain