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  9745  hashf1lem2  11286  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  ismgmid  13697  eqger  14027  eqgid  14029  znleval  14988  bastop2  15185  restopn2  15284  restdis  15285  tx1cn  15370  tx2cn  15371  imasnopn  15400  xmeter  15537  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  eupth2lem2dc  16700  eupth2lemsfi  16719