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  3304  rexss  3305  reuhypd  4592  elxp4  5250  elxp5  5251  dfco2a  5263  feu  5549  funbrfv2b  5721  dffn5im  5722  eqfnfv2  5776  dff4im  5823  fmptco  5843  dff13  5941  f1od2  6431  mpoxopovel  6472  brtposg  6485  dftpos3  6493  erinxp  6843  qliftfun  6851  pw2f1odclem  7087  genpdflem  7822  ltexprlemm  7915  prime  9677  oddnn02np1  12564  oddge22np1  12565  evennn02n  12566  evennn2n  12567  ismgmid  13588  eqger  13939  eqgid  13941  znleval  14799  bastop2  14947  restopn2  15046  restdis  15047  tx1cn  15132  tx2cn  15133  imasnopn  15162  xmeter  15299  lgsquadlem1  15948  lgsquadlem2  15949  lgsquadlem3  15950  eupth2lem2dc  16452  eupth2lemsfi  16471