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  4561  elxp4  5215  elxp5  5216  dfco2a  5228  feu  5507  funbrfv2b  5677  dffn5im  5678  eqfnfv2  5732  dff4im  5780  fmptco  5800  dff13  5891  f1od2  6379  mpoxopovel  6385  brtposg  6398  dftpos3  6406  erinxp  6754  qliftfun  6762  pw2f1odclem  6991  genpdflem  7690  ltexprlemm  7783  prime  9542  oddnn02np1  12386  oddge22np1  12387  evennn02n  12388  evennn2n  12389  ismgmid  13405  eqger  13756  eqgid  13758  znleval  14611  bastop2  14752  restopn2  14851  restdis  14852  tx1cn  14937  tx2cn  14938  imasnopn  14967  xmeter  15104  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752