Theorem pm5.74da 800

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  cbvaldvaw  2042  sb4b  2475  sb4bOLD  2476  ralbidva  3119  ralbidaOLD  3157  vtocl2d  3486  vtocl2  3490  vtocl3  3491  spc3egv  3532  ralxpxfr2d  3568  elabd2  3594  elrab3t  3616  csbie2df  4371  ordunisuc2  7666  dfom2  7689  pwfseqlem3  10347  lo1resb  15201  rlimresb  15202  o1resb  15203  fsumparts  15446  isprm3  16316  ramval  16637  islindf4  20955  cnntr  22334  fclsbas  23080  metcnp  23603  voliunlem3  24621  ellimc2  24946  limcflf  24950  mdegleb  25134  xrlimcnp  26023  dchrelbas3  26291  lmicom  27053  dmdbr5ati  30685  isarchi3  31343  islinds5  31465  cmpcref  31702  sscoid  34142  bj-equsalvwd  34889  cdlemefrs29bpre0  38337  cdlemkid3N  38874  cdlemkid4  38875  hdmap1eulem  39763  hdmap1eulemOLDN  39764  jm2.25  40737  ntrneik2  41591  ntrneix2  41592  ntrneikb  41593  fourierdlem87  43624