Theorem pm4.71 635

Description: Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120.

Assertion

Ref	Expression
pm4.71	|- ((ph -> ps) <-> (ph <-> (ph /\ ps)))

Proof of Theorem pm4.71

Step	Hyp	Ref	Expression
1		ancl 294	. . 3 |- ((ph -> ps) -> (ph -> (ph /\ ps)))
2		pm3.26 319	. . 3 |- ((ph /\ ps) -> ph)
3	1, 2	impbid1 517	. 2 |- ((ph -> ps) -> (ph <-> (ph /\ ps)))
4		bi1 148	. . 3 |- ((ph <-> (ph /\ ps)) -> (ph -> (ph /\ ps)))
5		pm3.27 323	. . 3 |- ((ph /\ ps) -> ps)
6	4, 5	syl6 22	. 2 |- ((ph <-> (ph /\ ps)) -> (ph -> ps))
7	3, 6	impbi 157	1 |- ((ph -> ps) <-> (ph <-> (ph /\ ps)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm4.71r 636  pm4.71i 637  bigolden 747  exintrbi 1118  rabid2 1770  dfss2 2058  disj3 2314  moabex 2766  dmopab3 3322  resopab2 3398  fcoi2 3646  fcnvres 3648  pw2en 4446  snunioolem 6414  pilem1 8671

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