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

Theorem ancomsd 470
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 ancom 466 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
2 ancomsd.1 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
31, 2syl5bi 232 1 (𝜑 → ((𝜒𝜓) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  sylan2d  499  mpand  711  anabsi6  859  ralcom2  3102  ralxfrdOLD  4878  somo  5067  wereu2  5109  poirr2  5518  smoel  7454  cfub  9068  cofsmo  9088  grudomon  9636  axpre-sup  9987  leltadd  10509  lemul12b  10877  lbzbi  11773  injresinj  12584  abslt  14048  absle  14049  o1lo1  14262  o1co  14311  rlimno1  14378  znnenlem  14934  dvdssub2  15017  lublecllem  16982  f1omvdco2  17862  ptpjpre1  21368  iocopnst  22733  ovolicc2lem4  23282  itg2le  23500  ulmcau  24143  cxpeq0  24418  pntrsumbnd2  25250  cvcon3  29127  atexch  29224  abfmpeld  29438  wsuclem  31757  wsuclemOLD  31758  btwntriv2  32103  btwnexch3  32111  isbasisrelowllem1  33183  isbasisrelowllem2  33184  relowlssretop  33191  finxpsuclem  33214  finixpnum  33374  fin2solem  33375  ltflcei  33377  poimirlem27  33416  itg2addnclem  33441  unirep  33487  prter2  33992  cvrcon3b  34390  incssnn0  37100  eldioph4b  37201  fphpdo  37207  pellexlem5  37223  pm14.24  38459  icceuelpart  41142  goldbachthlem2  41229  gbegt5  41420  prsprel  41508  sprsymrelfolem2  41514  aacllem  42318
  Copyright terms: Public domain W3C validator