Theorem pm4.71rd 392

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 388	. 2 |- ( ( ps -> ch ) <-> ( ps <-> ( ch /\ ps ) ) )
3	1, 2	sylib 121	1 |- ( ph -> ( ps <-> ( ch /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ralss  3213  rexss  3214  reuhypd  4456  elxp4  5098  elxp5  5099  dfco2a  5111  feu  5380  funbrfv2b  5541  dffn5im  5542  eqfnfv2  5594  dff4im  5642  fmptco  5662  dff13  5747  f1od2  6214  mpoxopovel  6220  brtposg  6233  dftpos3  6241  erinxp  6587  qliftfun  6595  genpdflem  7469  ltexprlemm  7562  prime  9311  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  ismgmid  12631  bastop2  12878  restopn2  12977  restdis  12978  tx1cn  13063  tx2cn  13064  imasnopn  13093  xmeter  13230