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  3249  rexss  3250  reuhypd  4506  elxp4  5157  elxp5  5158  dfco2a  5170  feu  5440  funbrfv2b  5605  dffn5im  5606  eqfnfv2  5660  dff4im  5708  fmptco  5728  dff13  5815  f1od2  6293  mpoxopovel  6299  brtposg  6312  dftpos3  6320  erinxp  6668  qliftfun  6676  pw2f1odclem  6895  genpdflem  7574  ltexprlemm  7667  prime  9425  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  ismgmid  13020  eqger  13354  eqgid  13356  znleval  14209  bastop2  14320  restopn2  14419  restdis  14420  tx1cn  14505  tx2cn  14506  imasnopn  14535  xmeter  14672  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320