Theorem pm4.71 633

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 515	. 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 634  pm4.71i 635  bigolden 745  exintrbi 1114  rabid2 1762  dfss2 2048  disj3 2304  moabex 2756  dmopab3 3311  resopab2 3382  fcoi2 3631  fcnvres 3633  pw2en 4426  snunioolem 6347  pilem1 8590

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