Theorem pm5.74da 804

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  2040  sb4b  2480  ralbidva  3159  cbvraldva  3218  vtocl2d  3521  vtocl2  3524  vtocl3  3525  spc3egv  3559  ralxpxfr2d  3602  elabd2  3626  elrab3t  3647  csbie2df  4397  ordunisuc2  7796  dfom2  7820  pwfseqlem3  10583  lo1resb  15499  rlimresb  15500  o1resb  15501  fsumparts  15741  isprm3  16622  ramval  16948  islindf4  21805  cnntr  23231  fclsbas  23977  metcnp  24497  voliunlem3  25521  ellimc2  25846  limcflf  25850  mdegleb  26037  xrlimcnp  26946  dchrelbas3  27217  lmicom  28872  dmdbr5ati  32510  isarchi3  33281  islinds5  33460  cmpcref  34028  sscoid  36127  regsfromregtr  36690  bj-equsalvwd  37015  cdlemefrs29bpre0  40772  cdlemkid3N  41309  cdlemkid4  41310  hdmap1eulem  42198  hdmap1eulemOLDN  42199  jm2.25  43356  ntrneik2  44448  ntrneix2  44449  ntrneikb  44450  fourierdlem87  46551