Theorem pm5.74da 801

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  cbvaldvaw  2040  sb4b  2473  sb4bOLD  2474  ralbidva  3168  ralbidaOLD  3250  vtocl2d  3505  vtocl2  3509  vtocl3  3510  spc3egv  3551  ralxpxfr2d  3585  elabd2  3611  elrab3t  3633  csbie2df  4386  ordunisuc2  7750  dfom2  7774  pwfseqlem3  10509  lo1resb  15364  rlimresb  15365  o1resb  15366  fsumparts  15609  isprm3  16477  ramval  16798  islindf4  21143  cnntr  22524  fclsbas  23270  metcnp  23795  voliunlem3  24814  ellimc2  25139  limcflf  25143  mdegleb  25327  xrlimcnp  26216  dchrelbas3  26484  lmicom  27379  dmdbr5ati  31013  isarchi3  31669  islinds5  31801  cmpcref  32039  sscoid  34306  bj-equsalvwd  35053  cdlemefrs29bpre0  38657  cdlemkid3N  39194  cdlemkid4  39195  hdmap1eulem  40083  hdmap1eulemOLDN  40084  jm2.25  41072  ntrneik2  42012  ntrneix2  42013  ntrneikb  42014  fourierdlem87  44059