Theorem pm4.71rd 374

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 370	. 2 ⊢ ((ψ → χ) ↔ (ψ ↔ (χ ∧ ψ)))
3	1, 2	sylib 127	1 ⊢ (φ → (ψ ↔ (χ ∧ ψ)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ralss  3000  rexss  3001  reuhypd  4169  elxp4  4751  elxp5  4752  dfco2a  4764  feu  5015  funbrfv2b  5161  dffn5im  5162  eqfnfv2  5209  dff4im  5256  fmptco  5273  dff13  5350  mpt2xopovel  5797  brtposg  5810  dftpos3  5818  erinxp  6116  qliftfun  6124  genpdflem  6490  ltexprlemm  6574  prime  8113