Theorem pm5.74da 816

Description: Distribution of implication over biconditional (deduction form). Variant of pm5.74d 276. (Contributed by NM, 4-May-2007.)

Hypothesis

Ref	Expression
pm5.74da.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
pm5.74da	⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Proof of Theorem pm5.74da

Step	Hyp	Ref	Expression
1		pm5.74da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	ex 418	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.74d 276	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cbvaldvaw  2071  sb4b  2509  ralbidva  3188  cbvraldva  3247  vtocl2d  3530  vtocl2  3533  vtocl3  3534  spc3egv  3564  ralxpxfr2d  3607  elabd2  3631  elrab3t  3651  csbie2df  4408  ordunisuc2  7842  dfom2  7866  pwfseqlem3  10656  lo1resb  15635  rlimresb  15636  o1resb  15637  fsumparts  15877  isprm3  16759  ramval  17086  islindf4  22018  cnntr  23462  fclsbas  24209  metcnp  24729  voliunlem3  25742  ellimc2  26067  limcflf  26071  mdegleb  26252  xrlimcnp  27164  dchrelbas3  27433  elplng  29093  plngcplem  29098  lmicom  29128  dmdbr5ati  32821  isarchi3  33547  islinds5  33722  cmpcref  34280  sscoid  36416  regsfromregtco  37082  bj-equsalvwd  37430  cdlemefrs29bpre0  41203  cdlemkid3N  41740  cdlemkid4  41741  hdmap1eulem  42629  hdmap1eulemOLDN  42630  jm2.25  43759  ntrneik2  44851  ntrneix2  44852  ntrneikb  44853  fourierdlem87  46940