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  3294  rexss  3295  reuhypd  4574  elxp4  5231  elxp5  5232  dfco2a  5244  feu  5527  funbrfv2b  5699  dffn5im  5700  eqfnfv2  5754  dff4im  5801  fmptco  5821  dff13  5919  f1od2  6409  mpoxopovel  6450  brtposg  6463  dftpos3  6471  erinxp  6821  qliftfun  6829  pw2f1odclem  7063  genpdflem  7770  ltexprlemm  7863  prime  9623  oddnn02np1  12504  oddge22np1  12505  evennn02n  12506  evennn2n  12507  ismgmid  13523  eqger  13874  eqgid  13876  znleval  14732  bastop2  14878  restopn2  14977  restdis  14978  tx1cn  15063  tx2cn  15064  imasnopn  15093  xmeter  15230  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  eupth2lem2dc  16383  eupth2lemsfi  16402