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  3304  rexss  3305  reuhypd  4592  elxp4  5250  elxp5  5251  dfco2a  5263  feu  5549  funbrfv2b  5721  dffn5im  5722  eqfnfv2  5776  dff4im  5823  fmptco  5843  dff13  5941  f1od2  6431  mpoxopovel  6472  brtposg  6485  dftpos3  6493  erinxp  6843  qliftfun  6851  pw2f1odclem  7087  genpdflem  7822  ltexprlemm  7915  prime  9677  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  ismgmid  13590  eqger  13941  eqgid  13943  znleval  14801  bastop2  14949  restopn2  15048  restdis  15049  tx1cn  15134  tx2cn  15135  imasnopn  15164  xmeter  15301  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  eupth2lem2dc  16454  eupth2lemsfi  16473