Theorem pm5.74da 803

Description: Distribution of implication over biconditional (deduction form). Variant of pm5.74d 273. (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 412	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.74d 273	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  cbvaldvaw  2037  sb4b  2479  ralbidva  3161  cbvraldva  3222  vtocl2d  3541  vtocl2  3545  vtocl3  3546  spc3egv  3582  ralxpxfr2d  3625  elabd2  3649  elrab3t  3670  csbie2df  4418  ordunisuc2  7837  dfom2  7861  pwfseqlem3  10672  lo1resb  15578  rlimresb  15579  o1resb  15580  fsumparts  15820  isprm3  16700  ramval  17026  islindf4  21796  cnntr  23211  fclsbas  23957  metcnp  24478  voliunlem3  25503  ellimc2  25828  limcflf  25832  mdegleb  26019  xrlimcnp  26928  dchrelbas3  27199  lmicom  28713  dmdbr5ati  32349  isarchi3  33131  islinds5  33328  cmpcref  33827  sscoid  35877  bj-equsalvwd  36744  cdlemefrs29bpre0  40361  cdlemkid3N  40898  cdlemkid4  40899  hdmap1eulem  41787  hdmap1eulemOLDN  41788  jm2.25  42970  ntrneik2  44063  ntrneix2  44064  ntrneikb  44065  fourierdlem87  46170