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  3222  rexss  3223  reuhypd  4472  elxp4  5117  elxp5  5118  dfco2a  5130  feu  5399  funbrfv2b  5561  dffn5im  5562  eqfnfv2  5615  dff4im  5663  fmptco  5683  dff13  5769  f1od2  6236  mpoxopovel  6242  brtposg  6255  dftpos3  6263  erinxp  6609  qliftfun  6617  genpdflem  7506  ltexprlemm  7599  prime  9352  oddnn02np1  11885  oddge22np1  11886  evennn02n  11887  evennn2n  11888  ismgmid  12796  eqger  13083  eqgid  13085  bastop2  13587  restopn2  13686  restdis  13687  tx1cn  13772  tx2cn  13773  imasnopn  13802  xmeter  13939