Theorem pm5.74da 802

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 415	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.74d 275	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

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

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 399

This theorem is referenced by:  cbvaldvaw  2045  sb4b  2499  sb4bOLD  2500  ralbidva  3196  ralbida  3230  vtocl2d  3557  vtocl2  3561  vtocl3  3563  spc3egv  3604  ralxpxfr2d  3639  elrab3t  3679  vtocl2dOLD  3931  csbie2df  4392  ordunisuc2  7559  dfom2  7582  pwfseqlem3  10082  lo1resb  14921  rlimresb  14922  o1resb  14923  fsumparts  15161  isprm3  16027  ramval  16344  islindf4  20982  cnntr  21883  fclsbas  22629  metcnp  23151  voliunlem3  24153  ellimc2  24475  limcflf  24479  mdegleb  24658  xrlimcnp  25546  dchrelbas3  25814  lmicom  26574  dmdbr5ati  30199  isarchi3  30816  islinds5  30932  cmpcref  31114  sscoid  33374  cdlemefrs29bpre0  37547  cdlemkid3N  38084  cdlemkid4  38085  hdmap1eulem  38973  hdmap1eulemOLDN  38974  jm2.25  39616  ntrneik2  40462  ntrneix2  40463  ntrneikb  40464  fourierdlem87  42498