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  3250  rexss  3251  reuhypd  4507  elxp4  5158  elxp5  5159  dfco2a  5171  feu  5443  funbrfv2b  5608  dffn5im  5609  eqfnfv2  5663  dff4im  5711  fmptco  5731  dff13  5818  f1od2  6302  mpoxopovel  6308  brtposg  6321  dftpos3  6329  erinxp  6677  qliftfun  6685  pw2f1odclem  6904  genpdflem  7591  ltexprlemm  7684  prime  9442  oddnn02np1  12062  oddge22np1  12063  evennn02n  12064  evennn2n  12065  ismgmid  13079  eqger  13430  eqgid  13432  znleval  14285  bastop2  14404  restopn2  14503  restdis  14504  tx1cn  14589  tx2cn  14590  imasnopn  14619  xmeter  14756  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404