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  3291  rexss  3292  reuhypd  4566  elxp4  5222  elxp5  5223  dfco2a  5235  feu  5516  funbrfv2b  5686  dffn5im  5687  eqfnfv2  5741  dff4im  5789  fmptco  5809  dff13  5904  f1od2  6395  mpoxopovel  6402  brtposg  6415  dftpos3  6423  erinxp  6773  qliftfun  6781  pw2f1odclem  7015  genpdflem  7717  ltexprlemm  7810  prime  9569  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  ismgmid  13450  eqger  13801  eqgid  13803  znleval  14657  bastop2  14798  restopn2  14897  restdis  14898  tx1cn  14983  tx2cn  14984  imasnopn  15013  xmeter  15150  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798