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  3294  rexss  3295  reuhypd  4574  elxp4  5231  elxp5  5232  dfco2a  5244  feu  5527  funbrfv2b  5699  dffn5im  5700  eqfnfv2  5754  dff4im  5801  fmptco  5821  dff13  5919  f1od2  6409  mpoxopovel  6450  brtposg  6463  dftpos3  6471  erinxp  6821  qliftfun  6829  pw2f1odclem  7063  genpdflem  7787  ltexprlemm  7880  prime  9640  oddnn02np1  12521  oddge22np1  12522  evennn02n  12523  evennn2n  12524  ismgmid  13540  eqger  13891  eqgid  13893  znleval  14749  bastop2  14895  restopn2  14994  restdis  14995  tx1cn  15080  tx2cn  15081  imasnopn  15110  xmeter  15247  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  eupth2lem2dc  16400  eupth2lemsfi  16419