Theorem pm4.71rd 398

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 394	. 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  3314  rexss  3315  reuhypd  4612  elxp4  5270  elxp5  5271  dfco2a  5283  feu  5569  funbrfv2b  5741  dffn5im  5742  eqfnfv2  5798  dff4im  5845  fmptco  5865  dff13  5964  f1od2  6461  mpoxopovel  6502  brtposg  6515  dftpos3  6523  erinxp  6873  qliftfun  6881  pw2f1odclem  7124  genpdflem  7864  ltexprlemm  7957  prime  9724  hashf1lem2  11264  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  ismgmid  13674  eqger  14004  eqgid  14006  znleval  14960  bastop2  15108  restopn2  15207  restdis  15208  tx1cn  15293  tx2cn  15294  imasnopn  15323  xmeter  15460  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  eupth2lem2dc  16614  eupth2lemsfi  16633