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  3246  rexss  3247  reuhypd  4503  elxp4  5154  elxp5  5155  dfco2a  5167  feu  5437  funbrfv2b  5602  dffn5im  5603  eqfnfv2  5657  dff4im  5705  fmptco  5725  dff13  5812  f1od2  6290  mpoxopovel  6296  brtposg  6309  dftpos3  6317  erinxp  6665  qliftfun  6673  pw2f1odclem  6892  genpdflem  7569  ltexprlemm  7662  prime  9419  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  ismgmid  12963  eqger  13297  eqgid  13299  znleval  14152  bastop2  14263  restopn2  14362  restdis  14363  tx1cn  14448  tx2cn  14449  imasnopn  14478  xmeter  14615  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236