Theorem pm4.71 697

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 318	. . 3 |- ((ph -> ps) -> (ph -> (ph /\ ps)))
2		simpl 346	. . 3 |- ((ph /\ ps) -> ph)
3	1, 2	impbid1 575	. 2 |- ((ph -> ps) -> (ph <-> (ph /\ ps)))
4		bi1 165	. . 3 |- ((ph <-> (ph /\ ps)) -> (ph -> (ph /\ ps)))
5		simpr 350	. . 3 |- ((ph /\ ps) -> ps)
6	4, 5	syl6 25	. 2 |- ((ph <-> (ph /\ ps)) -> (ph -> ps))
7	3, 6	impbii 174	1 |- ((ph -> ps) <-> (ph <-> (ph /\ ps)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  pm4.71r 698  pm4.71i 699  bigolden 819  exintrbi 1476  rabid2 2254  rabid2OLD 2255  dfss2 2610  disj3 2918  moabex 3513  dmopab3 4169  resopab2 4256  fcoi2OLD 4587  fcnvres 4589  pw2en 5505  snunioolem 7583  pilem1 10020  usinuniop 10341  vtarsuelt 15272  difin2 15676  resoprab2 15710  isidlc 16163  erex 16262

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 164  df-an 242

Copyright terms: Public domain