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  2479  ralbidva  3157  cbvraldva  3216  vtocl2d  3519  vtocl2  3522  vtocl3  3523  spc3egv  3557  ralxpxfr2d  3600  elabd2  3624  elrab3t  3645  csbie2df  4395  ordunisuc2  7786  dfom2  7810  pwfseqlem3  10571  lo1resb  15487  rlimresb  15488  o1resb  15489  fsumparts  15729  isprm3  16610  ramval  16936  islindf4  21793  cnntr  23219  fclsbas  23965  metcnp  24485  voliunlem3  25509  ellimc2  25834  limcflf  25838  mdegleb  26025  xrlimcnp  26934  dchrelbas3  27205  lmicom  28860  dmdbr5ati  32497  isarchi3  33269  islinds5  33448  cmpcref  34007  sscoid  36105  regsfromregtr  36668  bj-equsalvwd  36981  cdlemefrs29bpre0  40656  cdlemkid3N  41193  cdlemkid4  41194  hdmap1eulem  42082  hdmap1eulemOLDN  42083  jm2.25  43241  ntrneik2  44333  ntrneix2  44334  ntrneikb  44335  fourierdlem87  46437