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  710  anabsi6  858  ralcom2  3099  ralxfrdOLD  4871  somo  5059  wereu2  5101  poirr2  5508  smoel  7442  cfub  9056  cofsmo  9076  grudomon  9624  axpre-sup  9975  leltadd  10497  lemul12b  10865  lbzbi  11761  injresinj  12572  abslt  14035  absle  14036  o1lo1  14249  o1co  14298  rlimno1  14365  znnenlem  14921  dvdssub2  15004  lublecllem  16969  f1omvdco2  17849  ptpjpre1  21355  iocopnst  22720  ovolicc2lem4  23269  itg2le  23487  ulmcau  24130  cxpeq0  24405  pntrsumbnd2  25237  cvcon3  29113  atexch  29210  abfmpeld  29427  wsuclem  31747  wsuclemOLD  31748  btwntriv2  32094  btwnexch3  32102  isbasisrelowllem1  33174  isbasisrelowllem2  33175  relowlssretop  33182  finxpsuclem  33205  finixpnum  33365  fin2solem  33366  ltflcei  33368  poimirlem27  33407  itg2addnclem  33432  unirep  33478  prter2  33985  cvrcon3b  34383  incssnn0  37093  eldioph4b  37194  fphpdo  37200  pellexlem5  37216  pm14.24  38453  icceuelpart  41136  goldbachthlem2  41223  gbegt5  41414  prsprel  41502  sprsymrelfolem2  41508  aacllem  42312
  Copyright terms: Public domain W3C validator