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  3290  rexss  3291  reuhypd  4562  elxp4  5216  elxp5  5217  dfco2a  5229  feu  5510  funbrfv2b  5680  dffn5im  5681  eqfnfv2  5735  dff4im  5783  fmptco  5803  dff13  5898  f1od2  6387  mpoxopovel  6393  brtposg  6406  dftpos3  6414  erinxp  6764  qliftfun  6772  pw2f1odclem  7003  genpdflem  7705  ltexprlemm  7798  prime  9557  oddnn02np1  12407  oddge22np1  12408  evennn02n  12409  evennn2n  12410  ismgmid  13426  eqger  13777  eqgid  13779  znleval  14633  bastop2  14774  restopn2  14873  restdis  14874  tx1cn  14959  tx2cn  14960  imasnopn  14989  xmeter  15126  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774