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  3263  rexss  3264  reuhypd  4531  elxp4  5184  elxp5  5185  dfco2a  5197  feu  5475  funbrfv2b  5641  dffn5im  5642  eqfnfv2  5696  dff4im  5744  fmptco  5764  dff13  5855  f1od2  6339  mpoxopovel  6345  brtposg  6358  dftpos3  6366  erinxp  6714  qliftfun  6722  pw2f1odclem  6951  genpdflem  7650  ltexprlemm  7743  prime  9502  oddnn02np1  12276  oddge22np1  12277  evennn02n  12278  evennn2n  12279  ismgmid  13294  eqger  13645  eqgid  13647  znleval  14500  bastop2  14641  restopn2  14740  restdis  14741  tx1cn  14826  tx2cn  14827  imasnopn  14856  xmeter  14993  lgsquadlem1  15639  lgsquadlem2  15640  lgsquadlem3  15641