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

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

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 395

This theorem is referenced by:  cbvaldvaw  2039  sb4b  2472  ralbidva  3173  cbvraldva  3234  ralbidaOLD  3266  vtocl2d  3548  vtocl2  3553  vtocl3  3554  spc3egv  3592  ralxpxfr2d  3633  elabd2  3659  elrab3t  3681  csbie2df  4439  ordunisuc2  7835  dfom2  7859  pwfseqlem3  10657  lo1resb  15512  rlimresb  15513  o1resb  15514  fsumparts  15756  isprm3  16624  ramval  16945  islindf4  21612  cnntr  22999  fclsbas  23745  metcnp  24270  voliunlem3  25301  ellimc2  25626  limcflf  25630  mdegleb  25817  xrlimcnp  26709  dchrelbas3  26977  lmicom  28306  dmdbr5ati  31942  isarchi3  32603  islinds5  32754  cmpcref  33128  sscoid  35189  bj-equsalvwd  35961  cdlemefrs29bpre0  39570  cdlemkid3N  40107  cdlemkid4  40108  hdmap1eulem  40996  hdmap1eulemOLDN  40997  jm2.25  42040  ntrneik2  43145  ntrneix2  43146  ntrneikb  43147  fourierdlem87  45207