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  3258  rexss  3259  reuhypd  4517  elxp4  5169  elxp5  5170  dfco2a  5182  feu  5457  funbrfv2b  5622  dffn5im  5623  eqfnfv2  5677  dff4im  5725  fmptco  5745  dff13  5836  f1od2  6320  mpoxopovel  6326  brtposg  6339  dftpos3  6347  erinxp  6695  qliftfun  6703  pw2f1odclem  6930  genpdflem  7619  ltexprlemm  7712  prime  9471  oddnn02np1  12162  oddge22np1  12163  evennn02n  12164  evennn2n  12165  ismgmid  13180  eqger  13531  eqgid  13533  znleval  14386  bastop2  14527  restopn2  14626  restdis  14627  tx1cn  14712  tx2cn  14713  imasnopn  14742  xmeter  14879  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527