Theorem pm5.74da 816

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cbvaldvaw  2071  sb4b  2505  ralbidva  3184  cbvraldva  3243  vtocl2d  3524  vtocl2  3527  vtocl3  3528  spc3egv  3558  ralxpxfr2d  3600  elabd2  3624  elrab3t  3644  csbie2df  4401  ordunisuc2  7853  dfom2  7877  pwfseqlem3  10738  lo1resb  15724  rlimresb  15725  o1resb  15726  fsumparts  15966  isprm3  16851  ramval  17179  islindf4  22137  cnntr  23586  fclsbas  24333  metcnp  24853  voliunlem3  25866  ellimc2  26190  limcflf  26194  mdegleb  26375  xrlimcnp  27289  dchrelbas3  27558  elplng  29251  plngcplem  29256  lmicom  29286  dmdbr5ati  33017  isarchi3  33741  islinds5  33916  cmpcref  34475  sscoid  36655  regsfromregtco  37306  bj-equsalvwd  37654  cdlemefrs29bpre0  41433  cdlemkid3N  41970  cdlemkid4  41971  hdmap1eulem  42859  hdmap1eulemOLDN  42860  jm2.25  43985  ntrneik2  45077  ntrneix2  45078  ntrneikb  45079  fourierdlem87  47172