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  3259  rexss  3260  reuhypd  4519  elxp4  5171  elxp5  5172  dfco2a  5184  feu  5460  funbrfv2b  5625  dffn5im  5626  eqfnfv2  5680  dff4im  5728  fmptco  5748  dff13  5839  f1od2  6323  mpoxopovel  6329  brtposg  6342  dftpos3  6350  erinxp  6698  qliftfun  6706  pw2f1odclem  6933  genpdflem  7622  ltexprlemm  7715  prime  9474  oddnn02np1  12224  oddge22np1  12225  evennn02n  12226  evennn2n  12227  ismgmid  13242  eqger  13593  eqgid  13595  znleval  14448  bastop2  14589  restopn2  14688  restdis  14689  tx1cn  14774  tx2cn  14775  imasnopn  14804  xmeter  14941  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589