Theorem pm4.71rd 386

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 382	. 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	sylib 120	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ralss  3087  rexss  3088  reuhypd  4293  elxp4  4918  elxp5  4919  dfco2a  4931  feu  5193  funbrfv2b  5349  dffn5im  5350  eqfnfv2  5398  dff4im  5445  fmptco  5464  dff13  5547  f1od2  6000  mpt2xopovel  6006  brtposg  6019  dftpos3  6027  erinxp  6366  qliftfun  6374  genpdflem  7066  ltexprlemm  7159  prime  8845  oddnn02np1  11158  oddge22np1  11159  evennn02n  11160  evennn2n  11161