Theorem pm5.74da 803

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  cbvaldvaw  2039  sb4b  2475  ralbidva  3153  cbvraldva  3212  vtocl2d  3515  vtocl2  3518  vtocl3  3519  spc3egv  3553  ralxpxfr2d  3596  elabd2  3620  elrab3t  3641  csbie2df  4388  ordunisuc2  7769  dfom2  7793  pwfseqlem3  10546  lo1resb  15466  rlimresb  15467  o1resb  15468  fsumparts  15708  isprm3  16589  ramval  16915  islindf4  21770  cnntr  23185  fclsbas  23931  metcnp  24451  voliunlem3  25475  ellimc2  25800  limcflf  25804  mdegleb  25991  xrlimcnp  26900  dchrelbas3  27171  lmicom  28761  dmdbr5ati  32394  isarchi3  33148  islinds5  33324  cmpcref  33855  sscoid  35947  bj-equsalvwd  36814  cdlemefrs29bpre0  40435  cdlemkid3N  40972  cdlemkid4  40973  hdmap1eulem  41861  hdmap1eulemOLDN  41862  jm2.25  43032  ntrneik2  44125  ntrneix2  44126  ntrneikb  44127  fourierdlem87  46231