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  3293  rexss  3294  reuhypd  4568  elxp4  5224  elxp5  5225  dfco2a  5237  feu  5519  funbrfv2b  5690  dffn5im  5691  eqfnfv2  5745  dff4im  5793  fmptco  5813  dff13  5908  f1od2  6399  mpoxopovel  6406  brtposg  6419  dftpos3  6427  erinxp  6777  qliftfun  6785  pw2f1odclem  7019  genpdflem  7726  ltexprlemm  7819  prime  9578  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  ismgmid  13459  eqger  13810  eqgid  13812  znleval  14666  bastop2  14807  restopn2  14906  restdis  14907  tx1cn  14992  tx2cn  14993  imasnopn  15022  xmeter  15159  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  eupth2lem2dc  16309