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  2039  sb4b  2477  ralbidva  3154  cbvraldva  3213  vtocl2d  3516  vtocl2  3519  vtocl3  3520  spc3egv  3554  ralxpxfr2d  3597  elabd2  3621  elrab3t  3642  csbie2df  4392  ordunisuc2  7783  dfom2  7807  pwfseqlem3  10562  lo1resb  15478  rlimresb  15479  o1resb  15480  fsumparts  15720  isprm3  16601  ramval  16927  islindf4  21784  cnntr  23210  fclsbas  23956  metcnp  24476  voliunlem3  25500  ellimc2  25825  limcflf  25829  mdegleb  26016  xrlimcnp  26925  dchrelbas3  27196  lmicom  28786  dmdbr5ati  32423  isarchi3  33197  islinds5  33376  cmpcref  33935  sscoid  36027  bj-equsalvwd  36897  cdlemefrs29bpre0  40568  cdlemkid3N  41105  cdlemkid4  41106  hdmap1eulem  41994  hdmap1eulemOLDN  41995  jm2.25  43156  ntrneik2  44249  ntrneix2  44250  ntrneikb  44251  fourierdlem87  46353