Theorem pm5.74da 816

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cbvaldvaw  2071  sb4b  2504  ralbidva  3183  cbvraldva  3242  vtocl2d  3523  vtocl2  3526  vtocl3  3527  spc3egv  3557  ralxpxfr2d  3600  elabd2  3624  elrab3t  3644  csbie2df  4401  ordunisuc2  7840  dfom2  7864  pwfseqlem3  10669  lo1resb  15651  rlimresb  15652  o1resb  15653  fsumparts  15893  isprm3  16773  ramval  17100  islindf4  22051  cnntr  23500  fclsbas  24247  metcnp  24767  voliunlem3  25780  ellimc2  26104  limcflf  26108  mdegleb  26289  xrlimcnp  27205  dchrelbas3  27474  elplng  29137  plngcplem  29142  lmicom  29172  dmdbr5ati  32903  isarchi3  33627  islinds5  33802  cmpcref  34360  sscoid  36490  regsfromregtco  37157  bj-equsalvwd  37505  cdlemefrs29bpre0  41269  cdlemkid3N  41806  cdlemkid4  41807  hdmap1eulem  42695  hdmap1eulemOLDN  42696  jm2.25  43840  ntrneik2  44932  ntrneix2  44933  ntrneikb  44934  fourierdlem87  47021