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  3245  rexss  3246  reuhypd  4502  elxp4  5153  elxp5  5154  dfco2a  5166  feu  5436  funbrfv2b  5601  dffn5im  5602  eqfnfv2  5656  dff4im  5704  fmptco  5724  dff13  5811  f1od2  6288  mpoxopovel  6294  brtposg  6307  dftpos3  6315  erinxp  6663  qliftfun  6671  pw2f1odclem  6890  genpdflem  7567  ltexprlemm  7660  prime  9416  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  ismgmid  12960  eqger  13294  eqgid  13296  znleval  14141  bastop2  14252  restopn2  14351  restdis  14352  tx1cn  14437  tx2cn  14438  imasnopn  14467  xmeter  14604  lgsquadlem1  15191