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  2510  ralbidva  3189  cbvraldva  3248  vtocl2d  3531  vtocl2  3534  vtocl3  3535  spc3egv  3565  ralxpxfr2d  3608  elabd2  3632  elrab3t  3652  csbie2df  4411  ordunisuc2  7849  dfom2  7873  pwfseqlem3  10663  lo1resb  15641  rlimresb  15642  o1resb  15643  fsumparts  15884  isprm3  16766  ramval  17093  islindf4  22018  cnntr  23462  fclsbas  24208  metcnp  24728  voliunlem3  25741  ellimc2  26066  limcflf  26070  mdegleb  26251  xrlimcnp  27163  dchrelbas3  27432  elplng  29092  plngcplem  29097  lmicom  29127  dmdbr5ati  32804  isarchi3  33531  islinds5  33706  cmpcref  34264  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