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  2073  sb4b  2507  ralbidva  3187  cbvraldva  3246  vtocl2d  3527  vtocl2  3530  vtocl3  3531  spc3egv  3561  ralxpxfr2d  3603  elabd2  3627  elrab3t  3647  csbie2df  4404  ordunisuc2  7887  dfom2  7911  pwfseqlem3  10782  lo1resb  15772  rlimresb  15773  o1resb  15774  fsumparts  16014  isprm3  16899  ramval  17227  islindf4  22188  cnntr  23637  fclsbas  24384  metcnp  24904  voliunlem3  25917  ellimc2  26241  limcflf  26245  mdegleb  26426  xrlimcnp  27342  dchrelbas3  27611  elplng  29304  plngcplem  29309  lmicom  29339  dmdbr5ati  33070  isarchi3  33837  islinds5  34020  cmpcref  34586  sscoid  36883  regsfromregtco  37534  bj-equsalvwd  37882  cdlemefrs29bpre0  41712  cdlemkid3N  42249  cdlemkid4  42250  hdmap1eulem  43138  hdmap1eulemOLDN  43139  jm2.25  44266  ntrneik2  45347  ntrneix2  45348  ntrneikb  45349  fourierdlem87  47470