Theorem pm5.74da 804

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  2040  sb4b  2480  ralbidva  3159  cbvraldva  3218  vtocl2d  3508  vtocl2  3511  vtocl3  3512  spc3egv  3546  ralxpxfr2d  3589  elabd2  3613  elrab3t  3634  csbie2df  4384  ordunisuc2  7788  dfom2  7812  pwfseqlem3  10574  lo1resb  15517  rlimresb  15518  o1resb  15519  fsumparts  15760  isprm3  16643  ramval  16970  islindf4  21828  cnntr  23250  fclsbas  23996  metcnp  24516  voliunlem3  25529  ellimc2  25854  limcflf  25858  mdegleb  26039  xrlimcnp  26945  dchrelbas3  27215  lmicom  28870  dmdbr5ati  32508  isarchi3  33263  islinds5  33442  cmpcref  34010  sscoid  36109  regsfromregtco  36736  bj-equsalvwd  37085  cdlemefrs29bpre0  40856  cdlemkid3N  41393  cdlemkid4  41394  hdmap1eulem  42282  hdmap1eulemOLDN  42283  jm2.25  43445  ntrneik2  44537  ntrneix2  44538  ntrneikb  44539  fourierdlem87  46639