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 555  19.26 1066  difrab 2270  opelopab2 2815  indpi 5017  lemulge11t 5814  lediv2it 5855  2climnn 7055  2climnn0 7056  climserzle 7100  alephexp2 7546  cnpco 7729  and4as 10390  and4com 10391

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