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  3168  rexss  3169  reuhypd  4400  elxp4  5034  elxp5  5035  dfco2a  5047  feu  5313  funbrfv2b  5474  dffn5im  5475  eqfnfv2  5527  dff4im  5574  fmptco  5594  dff13  5677  f1od2  6140  mpoxopovel  6146  brtposg  6159  dftpos3  6167  erinxp  6511  qliftfun  6519  genpdflem  7339  ltexprlemm  7432  prime  9174  oddnn02np1  11613  oddge22np1  11614  evennn02n  11615  evennn2n  11616  bastop2  12292  restopn2  12391  restdis  12392  tx1cn  12477  tx2cn  12478  imasnopn  12507  xmeter  12644