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  3290  rexss  3291  reuhypd  4562  elxp4  5216  elxp5  5217  dfco2a  5229  feu  5508  funbrfv2b  5678  dffn5im  5679  eqfnfv2  5733  dff4im  5781  fmptco  5801  dff13  5892  f1od2  6381  mpoxopovel  6387  brtposg  6400  dftpos3  6408  erinxp  6756  qliftfun  6764  pw2f1odclem  6995  genpdflem  7694  ltexprlemm  7787  prime  9546  oddnn02np1  12391  oddge22np1  12392  evennn02n  12393  evennn2n  12394  ismgmid  13410  eqger  13761  eqgid  13763  znleval  14617  bastop2  14758  restopn2  14857  restdis  14858  tx1cn  14943  tx2cn  14944  imasnopn  14973  xmeter  15110  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758