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  3293  rexss  3294  reuhypd  4568  elxp4  5224  elxp5  5225  dfco2a  5237  feu  5519  funbrfv2b  5690  dffn5im  5691  eqfnfv2  5745  dff4im  5793  fmptco  5813  dff13  5909  f1od2  6400  mpoxopovel  6407  brtposg  6420  dftpos3  6428  erinxp  6778  qliftfun  6786  pw2f1odclem  7020  genpdflem  7727  ltexprlemm  7820  prime  9579  oddnn02np1  12459  oddge22np1  12460  evennn02n  12461  evennn2n  12462  ismgmid  13478  eqger  13829  eqgid  13831  znleval  14686  bastop2  14827  restopn2  14926  restdis  14927  tx1cn  15012  tx2cn  15013  imasnopn  15042  xmeter  15179  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  eupth2lem2dc  16329  eupth2lemsfi  16348