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  3290  rexss  3291  reuhypd  4562  elxp4  5216  elxp5  5217  dfco2a  5229  feu  5510  funbrfv2b  5680  dffn5im  5681  eqfnfv2  5735  dff4im  5783  fmptco  5803  dff13  5898  f1od2  6387  mpoxopovel  6393  brtposg  6406  dftpos3  6414  erinxp  6764  qliftfun  6772  pw2f1odclem  7003  genpdflem  7705  ltexprlemm  7798  prime  9557  oddnn02np1  12406  oddge22np1  12407  evennn02n  12408  evennn2n  12409  ismgmid  13425  eqger  13776  eqgid  13778  znleval  14632  bastop2  14773  restopn2  14872  restdis  14873  tx1cn  14958  tx2cn  14959  imasnopn  14988  xmeter  15125  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773