Theorem pm5.74da 815

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  cbvaldvaw  2065  sb4b  2513  ralbidva  3192  cbvraldva  3251  vtocl2d  3537  vtocl2  3540  vtocl3  3541  spc3egv  3571  ralxpxfr2d  3614  elabd2  3638  elrab3t  3658  csbie2df  4406  ordunisuc2  7836  dfom2  7860  pwfseqlem3  10641  lo1resb  15611  rlimresb  15612  o1resb  15613  fsumparts  15854  isprm3  16737  ramval  17064  islindf4  21953  cnntr  23397  fclsbas  24143  metcnp  24663  voliunlem3  25676  ellimc2  26001  limcflf  26005  mdegleb  26186  xrlimcnp  27095  dchrelbas3  27364  elplng  29016  plngcplem  29021  lmicom  29051  dmdbr5ati  32711  isarchi3  33444  islinds5  33621  cmpcref  34181  sscoid  36298  regsfromregtco  36934  bj-equsalvwd  37282  cdlemefrs29bpre0  41055  cdlemkid3N  41592  cdlemkid4  41593  hdmap1eulem  42481  hdmap1eulemOLDN  42482  jm2.25  43613  ntrneik2  44705  ntrneix2  44706  ntrneikb  44707  fourierdlem87  46794