Theorem pm4.71rd 394

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ralss  3267  rexss  3268  reuhypd  4536  elxp4  5189  elxp5  5190  dfco2a  5202  feu  5480  funbrfv2b  5646  dffn5im  5647  eqfnfv2  5701  dff4im  5749  fmptco  5769  dff13  5860  f1od2  6344  mpoxopovel  6350  brtposg  6363  dftpos3  6371  erinxp  6719  qliftfun  6727  pw2f1odclem  6956  genpdflem  7655  ltexprlemm  7748  prime  9507  oddnn02np1  12306  oddge22np1  12307  evennn02n  12308  evennn2n  12309  ismgmid  13324  eqger  13675  eqgid  13677  znleval  14530  bastop2  14671  restopn2  14770  restdis  14771  tx1cn  14856  tx2cn  14857  imasnopn  14886  xmeter  15023  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671