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  4619  elxp4  5278  elxp5  5279  dfco2a  5291  feu  5577  funbrfv2b  5750  dffn5im  5751  eqfnfv2  5810  dff4im  5857  fmptco  5877  dff13  5977  f1od2  6475  mpoxopovel  6517  brtposg  6530  dftpos3  6538  erinxp  6888  qliftfun  6896  pw2f1odclem  7140  genpdflem  7880  ltexprlemm  7973  prime  9755  hashf1lem2  11307  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  ismgmid  13755  eqger  14085  eqgid  14087  znleval  15096  bastop2  15327  restopn2  15426  restdis  15427  tx1cn  15512  tx2cn  15513  imasnopn  15542  xmeter  15679  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  eupth2lem2dc  16922  eupth2lemsfi  16941