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

Theorem ancomsd 456
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 452 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
2 ancomsd.1 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
31, 2syl5bi 232 1 (𝜑 → ((𝜒𝜓) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  sylan2d  584  anabsi6  641  mpand  667  ralcom2  3251  ralxfrdOLD  5008  somo  5204  wereu2  5246  poirr2  5661  smoel  7609  cfub  9272  cofsmo  9292  grudomon  9840  axpre-sup  10191  leltadd  10713  lemul12b  11081  lbzbi  11978  injresinj  12796  abslt  14261  absle  14262  o1lo1  14475  o1co  14524  rlimno1  14591  znnenlem  15145  dvdssub2  15231  lublecllem  17195  f1omvdco2  18074  ptpjpre1  21594  iocopnst  22958  ovolicc2lem4  23507  itg2le  23725  ulmcau  24368  cxpeq0  24644  pntrsumbnd2  25476  cvcon3  29477  atexch  29574  abfmpeld  29788  wsuclem  32101  btwntriv2  32450  btwnexch3  32458  isbasisrelowllem1  33533  isbasisrelowllem2  33534  relowlssretop  33541  finxpsuclem  33564  finixpnum  33720  fin2solem  33721  ltflcei  33723  poimirlem27  33762  itg2addnclem  33786  unirep  33832  prter2  34682  cvrcon3b  35079  incssnn0  37793  eldioph4b  37894  fphpdo  37900  pellexlem5  37916  pm14.24  39152  icceuelpart  41890  goldbachthlem2  41976  gbegt5  42167  prsprel  42255  sprsymrelfolem2  42261  aacllem  43068
  Copyright terms: Public domain W3C validator