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  7875  ltexprlemm  7968  prime  9750  hashf1lem2  11302  oddnn02np1  12666  oddge22np1  12667  evennn02n  12668  evennn2n  12669  ismgmid  13750  eqger  14080  eqgid  14082  znleval  15072  bastop2  15276  restopn2  15375  restdis  15376  tx1cn  15461  tx2cn  15462  imasnopn  15491  xmeter  15628  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  eupth2lem2dc  16866  eupth2lemsfi  16885