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  3158  rexss  3159  reuhypd  4387  elxp4  5021  elxp5  5022  dfco2a  5034  feu  5300  funbrfv2b  5459  dffn5im  5460  eqfnfv2  5512  dff4im  5559  fmptco  5579  dff13  5662  f1od2  6125  mpoxopovel  6131  brtposg  6144  dftpos3  6152  erinxp  6496  qliftfun  6504  genpdflem  7308  ltexprlemm  7401  prime  9143  oddnn02np1  11566  oddge22np1  11567  evennn02n  11568  evennn2n  11569  bastop2  12242  restopn2  12341  restdis  12342  tx1cn  12427  tx2cn  12428  imasnopn  12457  xmeter  12594