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  2479  ralbidva  3158  cbvraldva  3217  vtocl2d  3507  vtocl2  3510  vtocl3  3511  spc3egv  3545  ralxpxfr2d  3588  elabd2  3612  elrab3t  3633  csbie2df  4383  ordunisuc2  7795  dfom2  7819  pwfseqlem3  10583  lo1resb  15526  rlimresb  15527  o1resb  15528  fsumparts  15769  isprm3  16652  ramval  16979  islindf4  21818  cnntr  23240  fclsbas  23986  metcnp  24506  voliunlem3  25519  ellimc2  25844  limcflf  25848  mdegleb  26029  xrlimcnp  26932  dchrelbas3  27201  lmicom  28856  dmdbr5ati  32493  isarchi3  33248  islinds5  33427  cmpcref  33994  sscoid  36093  regsfromregtco  36720  bj-equsalvwd  37069  cdlemefrs29bpre0  40842  cdlemkid3N  41379  cdlemkid4  41380  hdmap1eulem  42268  hdmap1eulemOLDN  42269  jm2.25  43427  ntrneik2  44519  ntrneix2  44520  ntrneikb  44521  fourierdlem87  46621