Theorem pm4.71rd 391

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	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
pm4.71rd	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Proof of Theorem pm4.71rd

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		pm4.71r 387	. 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	sylib 121	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ralss  3163  rexss  3164  reuhypd  4392  elxp4  5026  elxp5  5027  dfco2a  5039  feu  5305  funbrfv2b  5466  dffn5im  5467  eqfnfv2  5519  dff4im  5566  fmptco  5586  dff13  5669  f1od2  6132  mpoxopovel  6138  brtposg  6151  dftpos3  6159  erinxp  6503  qliftfun  6511  genpdflem  7315  ltexprlemm  7408  prime  9150  oddnn02np1  11577  oddge22np1  11578  evennn02n  11579  evennn2n  11580  bastop2  12253  restopn2  12352  restdis  12353  tx1cn  12438  tx2cn  12439  imasnopn  12468  xmeter  12605