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  2038  sb4b  2474  ralbidva  3155  cbvraldva  3218  vtocl2d  3531  vtocl2  3535  vtocl3  3536  spc3egv  3572  ralxpxfr2d  3615  elabd2  3639  elrab3t  3661  csbie2df  4409  ordunisuc2  7823  dfom2  7847  pwfseqlem3  10620  lo1resb  15537  rlimresb  15538  o1resb  15539  fsumparts  15779  isprm3  16660  ramval  16986  islindf4  21754  cnntr  23169  fclsbas  23915  metcnp  24436  voliunlem3  25460  ellimc2  25785  limcflf  25789  mdegleb  25976  xrlimcnp  26885  dchrelbas3  27156  lmicom  28722  dmdbr5ati  32358  isarchi3  33148  islinds5  33345  cmpcref  33847  sscoid  35908  bj-equsalvwd  36775  cdlemefrs29bpre0  40397  cdlemkid3N  40934  cdlemkid4  40935  hdmap1eulem  41823  hdmap1eulemOLDN  41824  jm2.25  42995  ntrneik2  44088  ntrneix2  44089  ntrneikb  44090  fourierdlem87  46198