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  2983  rexss  2984  reuhypd  4153  elxp4  4735  elxp5  4736  dfco2a  4748  feu  4997  funbrfv2b  5143  dffn5im  5144  eqfnfv2  5191  dff4im  5238  fmptco  5255  dff13  5332  mpt2xopovel  5778  brtposg  5791  dftpos3  5799  erinxp  6091  qliftfun  6099  genpdflem  6361  ltexprlemm  6437