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  3259  rexss  3260  reuhypd  4518  elxp4  5170  elxp5  5171  dfco2a  5183  feu  5458  funbrfv2b  5623  dffn5im  5624  eqfnfv2  5678  dff4im  5726  fmptco  5746  dff13  5837  f1od2  6321  mpoxopovel  6327  brtposg  6340  dftpos3  6348  erinxp  6696  qliftfun  6704  pw2f1odclem  6931  genpdflem  7620  ltexprlemm  7713  prime  9472  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  ismgmid  13209  eqger  13560  eqgid  13562  znleval  14415  bastop2  14556  restopn2  14655  restdis  14656  tx1cn  14741  tx2cn  14742  imasnopn  14771  xmeter  14908  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556