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

Theorem ancomsd 466
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 ancomsd.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expcomd 417 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
32impd 411 1 (𝜑 → ((𝜒𝜓) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  sylan2d  604  anabsi6  666  mpand  691  2eu3  2732  ralcom2w  3360  ralcom2  3361  somo  5503  wereu2  5545  smoel  7986  cfub  9659  cofsmo  9679  grudomon  10227  axpre-sup  10579  leltadd  11112  lemul12b  11485  lbzbi  12324  injresinj  13146  swrdnnn0nd  14006  abslt  14662  absle  14663  o1lo1  14882  o1co  14931  rlimno1  14998  dvdssub2  15639  lublecllem  17586  f1omvdco2  18505  ptpjpre1  22107  iocopnst  23471  ovolicc2lem4  24048  itg2le  24267  ulmcau  24910  cxpeq0  25188  pntrsumbnd2  26070  cvcon3  29988  atexch  30085  abfmpeld  30327  wsuclem  33009  btwntriv2  33370  btwnexch3  33378  isbasisrelowllem1  34518  isbasisrelowllem2  34519  relowlssretop  34526  finxpsuclem  34560  isinf2  34568  finixpnum  34758  fin2solem  34759  ltflcei  34761  poimirlem27  34800  itg2addnclem  34824  unirep  34869  prter2  35897  cvrcon3b  36293  incssnn0  39186  eldioph4b  39286  fphpdo  39292  pellexlem5  39308  pm14.24  40641  icceuelpart  43473  prsprel  43526  sprsymrelfolem2  43532  goldbachthlem2  43585  gbegt5  43803  aacllem  44830
  Copyright terms: Public domain W3C validator