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  3250  rexss  3251  reuhypd  4507  elxp4  5158  elxp5  5159  dfco2a  5171  feu  5441  funbrfv2b  5606  dffn5im  5607  eqfnfv2  5661  dff4im  5709  fmptco  5729  dff13  5816  f1od2  6294  mpoxopovel  6300  brtposg  6313  dftpos3  6321  erinxp  6669  qliftfun  6677  pw2f1odclem  6896  genpdflem  7576  ltexprlemm  7669  prime  9427  oddnn02np1  12047  oddge22np1  12048  evennn02n  12049  evennn2n  12050  ismgmid  13030  eqger  13364  eqgid  13366  znleval  14219  bastop2  14330  restopn2  14429  restdis  14430  tx1cn  14515  tx2cn  14516  imasnopn  14545  xmeter  14682  lgsquadlem1  15328  lgsquadlem2  15329  lgsquadlem3  15330