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  2037  sb4b  2483  ralbidva  3182  cbvraldva  3245  ralbidaOLD  3277  vtocl2d  3574  vtocl2  3578  vtocl3  3579  spc3egv  3616  ralxpxfr2d  3659  elabd2  3683  elrab3t  3707  csbie2df  4466  ordunisuc2  7881  dfom2  7905  pwfseqlem3  10729  lo1resb  15610  rlimresb  15611  o1resb  15612  fsumparts  15854  isprm3  16730  ramval  17055  islindf4  21881  cnntr  23304  fclsbas  24050  metcnp  24575  voliunlem3  25606  ellimc2  25932  limcflf  25936  mdegleb  26123  xrlimcnp  27029  dchrelbas3  27300  lmicom  28814  dmdbr5ati  32454  isarchi3  33167  islinds5  33360  cmpcref  33796  sscoid  35877  bj-equsalvwd  36746  cdlemefrs29bpre0  40353  cdlemkid3N  40890  cdlemkid4  40891  hdmap1eulem  41779  hdmap1eulemOLDN  41780  jm2.25  42956  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  fourierdlem87  46114