MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancomsd Structured version   Visualization version   GIF version

Theorem ancomsd 465
Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
Hypothesis
Ref Expression
ancomsd.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
ancomsd (𝜑 → ((𝜒𝜓) → 𝜃))

Proof of Theorem ancomsd
StepHypRef Expression
1 ancomsd.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expcomd 416 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
32impd 410 1 (𝜑 → ((𝜒𝜓) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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 206  df-an 396
This theorem is referenced by:  sylan2d  604  anabsi6  667  mpand  692  2eu3  2641  ralcom2  3365  somo  5615  wereu2  5663  smoel  8355  cfub  10239  cofsmo  10259  grudomon  10807  axpre-sup  11159  leltadd  11694  lemul12b  12067  lbzbi  12916  injresinj  13749  swrdnnn0nd  14602  abslt  15257  absle  15258  o1lo1  15477  o1co  15526  rlimno1  15596  dvdssub2  16240  lublecllem  18312  f1omvdco2  19353  ptpjpre1  23385  iocopnst  24774  ovolicc2lem4  25359  itg2le  25579  ulmcau  26236  cxpeq0  26516  pntrsumbnd2  27404  absslt  28047  cvcon3  31961  atexch  32058  abfmpeld  32303  wsuclem  35258  btwntriv2  35445  btwnexch3  35453  isbasisrelowllem1  36692  isbasisrelowllem2  36693  relowlssretop  36700  finxpsuclem  36734  isinf2  36742  finixpnum  36929  fin2solem  36930  ltflcei  36932  poimirlem27  36971  itg2addnclem  36995  unirep  37038  prter2  38207  cvrcon3b  38603  sn-negex12  41744  fltaccoprm  41837  incssnn0  41904  eldioph4b  42004  fphpdo  42010  pellexlem5  42026  pm14.24  43646  icceuelpart  46555  prsprel  46606  sprsymrelfolem2  46612  goldbachthlem2  46665  gbegt5  46880  aacllem  48002
  Copyright terms: Public domain W3C validator