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  3060  rexss  3061  reuhypd  4221  elxp4  4828  elxp5  4829  dfco2a  4841  feu  5092  funbrfv2b  5239  dffn5im  5240  eqfnfv2  5287  dff4im  5334  fmptco  5351  dff13  5428  f1od2  5876  mpt2xopovel  5879  brtposg  5892  dftpos3  5900  erinxp  6203  qliftfun  6211  genpdflem  6697  ltexprlemm  6790  prime  8446  oddnn02np1  10280  oddge22np1  10281  evennn02n  10282  evennn2n  10283