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  5909  f1od2  6400  mpoxopovel  6407  brtposg  6420  dftpos3  6428  erinxp  6778  qliftfun  6786  pw2f1odclem  7020  genpdflem  7727  ltexprlemm  7820  prime  9579  oddnn02np1  12446  oddge22np1  12447  evennn02n  12448  evennn2n  12449  ismgmid  13465  eqger  13816  eqgid  13818  znleval  14673  bastop2  14814  restopn2  14913  restdis  14914  tx1cn  14999  tx2cn  15000  imasnopn  15029  xmeter  15166  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  eupth2lem2dc  16316  eupth2lemsfi  16335