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  6516  brtposg  6529  dftpos3  6537  erinxp  6887  qliftfun  6895  pw2f1odclem  7138  genpdflem  7880  ltexprlemm  7973  prime  9756  hashf1lem2  11308  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  ismgmid  13756  eqger  14086  eqgid  14088  znleval  15097  bastop2  15310  restopn2  15409  restdis  15410  tx1cn  15495  tx2cn  15496  imasnopn  15525  xmeter  15662  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  eupth2lem2dc  16905  eupth2lemsfi  16924