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

Theorem ancomsd 468
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 464 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
2 ancomsd.1 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
31, 2syl5bi 230 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 195  df-an 384
This theorem is referenced by:  sylan2d  497  mpand  706  anabsi6  854  ralcom2  3078  ralxfrdOLD  4797  somo  4979  wereu2  5021  poirr2  5422  smoel  7317  cfub  8927  cofsmo  8947  grudomon  9491  axpre-sup  9842  leltadd  10357  lemul12b  10725  lbzbi  11604  injresinj  12402  abslt  13844  absle  13845  o1lo1  14058  o1co  14107  rlimno1  14174  znnenlem  14721  dvdssub2  14803  lublecllem  16753  f1omvdco2  17633  ptpjpre1  21122  iocopnst  22474  ovolicc2lem4  23008  itg2le  23225  ulmcau  23866  cxpeq0  24137  pntrsumbnd2  24969  cvcon3  28329  atexch  28426  abfmpeld  28636  wsuclem  30819  wsuclemOLD  30820  nofulllem5  30907  btwntriv2  31091  btwnexch3  31099  isbasisrelowllem1  32178  isbasisrelowllem2  32179  relowlssretop  32186  finxpsuclem  32209  finixpnum  32363  fin2solem  32364  ltflcei  32366  poimirlem27  32405  itg2addnclem  32430  unirep  32476  prter2  32983  cvrcon3b  33381  incssnn0  36091  eldioph4b  36192  fphpdo  36198  pellexlem5  36214  pm14.24  37454  icceuelpart  39775  goldbachthlem2  39797  gbegt5  39984  aacllem  42315
  Copyright terms: Public domain W3C validator