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

Theorem ancomsd 457
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 233 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 198  df-an 385
This theorem is referenced by:  sylan2d  598  anabsi6  660  mpand  686  ralcom2  3251  somo  5232  wereu2  5274  smoel  7661  cfub  9324  cofsmo  9344  grudomon  9892  axpre-sup  10243  leltadd  10766  lemul12b  11134  lbzbi  11977  injresinj  12797  abslt  14341  absle  14342  o1lo1  14555  o1co  14604  rlimno1  14671  znnenlemOLD  15224  dvdssub2  15310  lublecllem  17256  f1omvdco2  18133  ptpjpre1  21654  iocopnst  23018  ovolicc2lem4  23578  itg2le  23797  ulmcau  24440  cxpeq0  24715  pntrsumbnd2  25547  cvcon3  29534  atexch  29631  abfmpeld  29839  wsuclem  32146  btwntriv2  32495  btwnexch3  32503  isbasisrelowllem1  33568  isbasisrelowllem2  33569  relowlssretop  33576  finxpsuclem  33599  finixpnum  33750  fin2solem  33751  ltflcei  33753  poimirlem27  33792  itg2addnclem  33816  unirep  33862  prter2  34769  cvrcon3b  35165  incssnn0  37884  eldioph4b  37985  fphpdo  37991  pellexlem5  38007  pm14.24  39238  icceuelpart  42038  goldbachthlem2  42066  gbegt5  42257  prsprel  42338  sprsymrelfolem2  42344  aacllem  43151
  Copyright terms: Public domain W3C validator