Theorem pm5.74da 813

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  cbvaldvaw  2057  sb4b  2505  ralbidva  3182  cbvraldva  3241  vtocl2d  3527  vtocl2  3530  vtocl3  3531  spc3egv  3561  ralxpxfr2d  3604  elabd2  3628  elrab3t  3648  csbie2df  4394  ordunisuc2  7819  dfom2  7843  pwfseqlem3  10612  lo1resb  15582  rlimresb  15583  o1resb  15584  fsumparts  15825  isprm3  16708  ramval  17035  islindf4  21878  cnntr  23323  fclsbas  24069  metcnp  24589  voliunlem3  25602  ellimc2  25927  limcflf  25931  mdegleb  26112  xrlimcnp  27021  dchrelbas3  27290  lmicom  28945  dmdbr5ati  32582  isarchi3  33328  islinds5  33514  cmpcref  34108  sscoid  36222  regsfromregtco  36859  bj-equsalvwd  37208  cdlemefrs29bpre0  40981  cdlemkid3N  41518  cdlemkid4  41519  hdmap1eulem  42407  hdmap1eulemOLDN  42408  jm2.25  43537  ntrneik2  44629  ntrneix2  44630  ntrneikb  44631  fourierdlem87  46728