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  2473  ralbidva  3154  cbvraldva  3217  vtocl2d  3528  vtocl2  3532  vtocl3  3533  spc3egv  3569  ralxpxfr2d  3612  elabd2  3636  elrab3t  3658  csbie2df  4406  ordunisuc2  7820  dfom2  7844  pwfseqlem3  10613  lo1resb  15530  rlimresb  15531  o1resb  15532  fsumparts  15772  isprm3  16653  ramval  16979  islindf4  21747  cnntr  23162  fclsbas  23908  metcnp  24429  voliunlem3  25453  ellimc2  25778  limcflf  25782  mdegleb  25969  xrlimcnp  26878  dchrelbas3  27149  lmicom  28715  dmdbr5ati  32351  isarchi3  33141  islinds5  33338  cmpcref  33840  sscoid  35901  bj-equsalvwd  36768  cdlemefrs29bpre0  40390  cdlemkid3N  40927  cdlemkid4  40928  hdmap1eulem  41816  hdmap1eulemOLDN  41817  jm2.25  42988  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  fourierdlem87  46191