Theorem pm5.74da 801

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

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

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 397

This theorem is referenced by:  cbvaldvaw  2041  sb4b  2475  sb4bOLD  2476  ralbidva  3111  ralbidaOLD  3160  vtocl2d  3496  vtocl2  3500  vtocl3  3501  spc3egv  3542  ralxpxfr2d  3576  elabd2  3601  elrab3t  3623  csbie2df  4374  ordunisuc2  7691  dfom2  7714  pwfseqlem3  10416  lo1resb  15273  rlimresb  15274  o1resb  15275  fsumparts  15518  isprm3  16388  ramval  16709  islindf4  21045  cnntr  22426  fclsbas  23172  metcnp  23697  voliunlem3  24716  ellimc2  25041  limcflf  25045  mdegleb  25229  xrlimcnp  26118  dchrelbas3  26386  lmicom  27149  dmdbr5ati  30784  isarchi3  31441  islinds5  31563  cmpcref  31800  sscoid  34215  bj-equsalvwd  34962  cdlemefrs29bpre0  38410  cdlemkid3N  38947  cdlemkid4  38948  hdmap1eulem  39836  hdmap1eulemOLDN  39837  jm2.25  40821  ntrneik2  41702  ntrneix2  41703  ntrneikb  41704  fourierdlem87  43734