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  3158  cbvraldva  3217  vtocl2d  3520  vtocl2  3523  vtocl3  3524  spc3egv  3558  ralxpxfr2d  3601  elabd2  3625  elrab3t  3646  csbie2df  4396  ordunisuc2  7788  dfom2  7812  pwfseqlem3  10575  lo1resb  15491  rlimresb  15492  o1resb  15493  fsumparts  15733  isprm3  16614  ramval  16940  islindf4  21797  cnntr  23223  fclsbas  23969  metcnp  24489  voliunlem3  25513  ellimc2  25838  limcflf  25842  mdegleb  26029  xrlimcnp  26938  dchrelbas3  27209  lmicom  28843  dmdbr5ati  32480  isarchi3  33250  islinds5  33429  cmpcref  33988  sscoid  36086  bj-equsalvwd  36956  cdlemefrs29bpre0  40693  cdlemkid3N  41230  cdlemkid4  41231  hdmap1eulem  42119  hdmap1eulemOLDN  42120  jm2.25  43277  ntrneik2  44369  ntrneix2  44370  ntrneikb  44371  fourierdlem87  46473