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  3250  rexss  3251  reuhypd  4507  elxp4  5158  elxp5  5159  dfco2a  5171  feu  5443  funbrfv2b  5608  dffn5im  5609  eqfnfv2  5663  dff4im  5711  fmptco  5731  dff13  5818  f1od2  6302  mpoxopovel  6308  brtposg  6321  dftpos3  6329  erinxp  6677  qliftfun  6685  pw2f1odclem  6904  genpdflem  7593  ltexprlemm  7686  prime  9444  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  ismgmid  13081  eqger  13432  eqgid  13434  znleval  14287  bastop2  14428  restopn2  14527  restdis  14528  tx1cn  14613  tx2cn  14614  imasnopn  14643  xmeter  14780  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428