Theorem pm4.71rd 398

Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)

Hypothesis

Ref	Expression
pm4.71rd.1	|- ( ph -> ( ps -> ch ) )

Assertion

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

Proof of Theorem pm4.71rd

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		pm4.71r 394	. 2 |- ( ( ps -> ch ) <-> ( ps <-> ( ch /\ ps ) ) )
3	1, 2	sylib 122	1 |- ( ph -> ( ps <-> ( ch /\ ps ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ralss  3314  rexss  3315  reuhypd  4617  elxp4  5275  elxp5  5276  dfco2a  5288  feu  5574  funbrfv2b  5747  dffn5im  5748  eqfnfv2  5807  dff4im  5854  fmptco  5874  dff13  5974  f1od2  6471  mpoxopovel  6512  brtposg  6525  dftpos3  6533  erinxp  6883  qliftfun  6891  pw2f1odclem  7134  genpdflem  7874  ltexprlemm  7967  prime  9749  hashf1lem2  11300  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  ismgmid  13746  eqger  14076  eqgid  14078  znleval  15037  bastop2  15234  restopn2  15333  restdis  15334  tx1cn  15419  tx2cn  15420  imasnopn  15449  xmeter  15586  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  eupth2lem2dc  16798  eupth2lemsfi  16817