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  3208  rexss  3209  reuhypd  4449  elxp4  5091  elxp5  5092  dfco2a  5104  feu  5370  funbrfv2b  5531  dffn5im  5532  eqfnfv2  5584  dff4im  5631  fmptco  5651  dff13  5736  f1od2  6203  mpoxopovel  6209  brtposg  6222  dftpos3  6230  erinxp  6575  qliftfun  6583  genpdflem  7448  ltexprlemm  7541  prime  9290  oddnn02np1  11817  oddge22np1  11818  evennn02n  11819  evennn2n  11820  ismgmid  12608  bastop2  12724  restopn2  12823  restdis  12824  tx1cn  12909  tx2cn  12910  imasnopn  12939  xmeter  13076