Theorem pm4.71rd 394

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 390	. 2 |- ( ( ps -> ch ) <-> ( ps <-> ( ch /\ ps ) ) )
3	1, 2	sylib 122	1 |- ( ph -> ( ps <-> ( ch /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ralss  3308  rexss  3309  reuhypd  4597  elxp4  5255  elxp5  5256  dfco2a  5268  feu  5554  funbrfv2b  5726  dffn5im  5727  eqfnfv2  5781  dff4im  5828  fmptco  5848  dff13  5947  f1od2  6444  mpoxopovel  6485  brtposg  6498  dftpos3  6506  erinxp  6856  qliftfun  6864  pw2f1odclem  7100  genpdflem  7838  ltexprlemm  7931  prime  9695  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  ismgmid  13640  eqger  13977  eqgid  13979  znleval  14927  bastop2  15075  restopn2  15174  restdis  15175  tx1cn  15260  tx2cn  15261  imasnopn  15290  xmeter  15427  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  eupth2lem2dc  16580  eupth2lemsfi  16599