Theorem pm5.74da 809

Description: Distribution of implication over biconditional (deduction form). Variant of pm5.74d 274. (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 274	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  cbvaldvaw  2045  sb4b  2483  ralbidva  3160  cbvraldva  3219  vtocl2d  3507  vtocl2  3510  vtocl3  3511  spc3egv  3541  ralxpxfr2d  3584  elabd2  3608  elrab3t  3628  csbie2df  4371  ordunisuc2  7784  dfom2  7808  pwfseqlem3  10574  lo1resb  15517  rlimresb  15518  o1resb  15519  fsumparts  15760  isprm3  16643  ramval  16970  islindf4  21813  cnntr  23258  fclsbas  24004  metcnp  24524  voliunlem3  25537  ellimc2  25862  limcflf  25866  mdegleb  26047  xrlimcnp  26950  dchrelbas3  27219  lmicom  28874  dmdbr5ati  32511  isarchi3  33268  islinds5  33450  cmpcref  34034  sscoid  36139  regsfromregtco  36766  bj-equsalvwd  37115  cdlemefrs29bpre0  40888  cdlemkid3N  41425  cdlemkid4  41426  hdmap1eulem  42314  hdmap1eulemOLDN  42315  jm2.25  43444  ntrneik2  44536  ntrneix2  44537  ntrneikb  44538  fourierdlem87  46636