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  3223  rexss  3224  reuhypd  4473  elxp4  5118  elxp5  5119  dfco2a  5131  feu  5400  funbrfv2b  5563  dffn5im  5564  eqfnfv2  5617  dff4im  5665  fmptco  5685  dff13  5772  f1od2  6239  mpoxopovel  6245  brtposg  6258  dftpos3  6266  erinxp  6612  qliftfun  6620  genpdflem  7509  ltexprlemm  7602  prime  9355  oddnn02np1  11888  oddge22np1  11889  evennn02n  11890  evennn2n  11891  ismgmid  12802  eqger  13089  eqgid  13091  bastop2  13724  restopn2  13823  restdis  13824  tx1cn  13909  tx2cn  13910  imasnopn  13939  xmeter  14076