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  3308  rexss  3309  reuhypd  4597  elxp4  5255  elxp5  5256  dfco2a  5268  feu  5554  funbrfv2b  5726  dffn5im  5727  eqfnfv2  5781  dff4im  5828  fmptco  5848  dff13  5947  f1od2  6444  mpoxopovel  6485  brtposg  6498  dftpos3  6506  erinxp  6856  qliftfun  6864  pw2f1odclem  7100  genpdflem  7838  ltexprlemm  7931  prime  9698  oddnn02np1  12594  oddge22np1  12595  evennn02n  12596  evennn2n  12597  ismgmid  13643  eqger  13980  eqgid  13982  znleval  14930  bastop2  15078  restopn2  15177  restdis  15178  tx1cn  15263  tx2cn  15264  imasnopn  15293  xmeter  15430  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  eupth2lem2dc  16583  eupth2lemsfi  16602