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

Theorem syl5com 31
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)
Hypotheses
Ref Expression
syl5com.1 (𝜑𝜓)
syl5com.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5com (𝜑 → (𝜒𝜃))

Proof of Theorem syl5com
StepHypRef Expression
1 syl5com.1 . . 3 (𝜑𝜓)
21a1d 25 . 2 (𝜑 → (𝜒𝜓))
3 syl5com.2 . 2 (𝜒 → (𝜓𝜃))
42, 3sylcom 30 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com12  32  syl5  34  speimfw  2045  axc16i  2472  eupickbi  2688  ceqsalgALT  3383  cgsexg  3390  cgsex2g  3391  cgsex4g  3392  spc2egv  3446  spc3egv  3448  disjne  4165  uneqdifeq  4199  preqsnd  4523  preq12nebg  4529  opthprneg  4531  relresfld  5806  unixpid  5814  ordnbtwn  5959  sucssel  5962  ordelinel  5968  fvimacnv  6475  2f1fvneq  6660  ordsuc  7161  tfi  7200  fornex  7282  f1ovv  7284  wfrlem4  7570  wfrlem4OLD  7571  wfrlem10  7577  tz7.49  7693  oeworde  7827  dom2d  8150  findcard  8355  fisupg  8364  dffi3  8493  fiinfg  8561  noinfep  8721  cantnflem2  8751  tcmin  8781  rankr1ag  8829  rankelb  8851  rankunb  8877  rankxpsuc  8909  alephordi  9097  alephsucdom  9102  alephinit  9118  dfac9  9160  ackbij2lem4  9266  cff1  9282  cfslbn  9291  cfcoflem  9296  cfcof  9298  infpssrlem5  9331  isfin7-2  9420  acncc  9464  domtriomlem  9466  axdc3lem2  9475  ttukeylem1  9533  iundom2g  9564  axpowndlem3  9623  wunex2  9762  grupr  9821  gruiun  9823  eltskm  9867  nqereu  9953  addcanpr  10070  axpre-sup  10192  relin01  10754  nneo  11663  zeo2  11666  xrub  12347  uznfz  12630  difelfzle  12660  ssfzo12  12769  facndiv  13279  hashgt12el2  13413  hash2prde  13454  hash2pwpr  13460  hashle2prv  13462  fi1uzind  13481  swrdswrd  13669  swrdccatin2  13696  swrdccatin12lem2  13698  swrdccatin12  13700  swrdccat3  13701  swrdccatid  13706  repswswrd  13740  2cshwcshw  13780  relexpcnvd  13984  relexpdmd  13992  relexprnd  13996  relexpfldd  13998  relexpaddd  14002  fsumcom2  14713  fprodss  14885  fprodcom2  14921  sumodd  15319  ndvdssub  15341  eucalglt  15506  prmind2  15605  coprm  15630  prmdiveq  15698  prmdvdsprmop  15954  prmgaplem5  15966  drsdir  17143  lublecllem  17196  istos  17243  tsrlin  17427  dirge  17445  mhmlin  17550  issubg2  17817  nsgbi  17833  symgextf1lem  18047  sylow2a  18241  issubrg2  19010  abvmul  19039  abvtri  19040  lmodlema  19078  rmodislmodlem  19140  rmodislmod  19141  lspsnel6  19207  lmhmlin  19248  lbsind  19293  0ring01eq  19486  01eq0ring  19487  ipcj  20196  obsip  20282  lindsss  20380  mamufacex  20412  mavmulsolcl  20575  slesolvec  20704  inopn  20924  basis1  20975  tgss  20993  tgcl  20994  elcls3  21108  neindisj2  21148  cncls  21299  1stcelcls  21485  qtoptop2  21723  nrmr0reg  21773  fbasssin  21860  fbfinnfr  21865  fbunfip  21893  filufint  21944  uffix  21945  ufinffr  21953  ufilen  21954  fmfnfmlem1  21978  flftg  22020  alexsubALT  22075  xmeteq0  22363  blssexps  22451  blssex  22452  mopni3  22519  neibl  22526  metss  22533  metcnp3  22565  nmvs  22700  reperflem  22841  iccntr  22844  reconnlem2  22850  lebnumlem3  22982  caubl  23325  bcthlem5  23344  ovolunlem1  23485  voliunlem1  23538  volsuplem  23543  ellimc3  23863  lhop1lem  23996  ulmss  24371  lgsqrmodndvds  25299  2lgsoddprmlem3  25360  dchrisumlema  25398  umgrnloopv  26222  usgrnloopvALT  26315  umgrres1lem  26425  upgrres1  26428  nbuhgr  26462  cplgrop  26568  fusgrregdegfi  26700  g0wlk0  26783  wlkdlem2  26815  upgrwlkdvdelem  26867  crctcshwlkn0lem4  26941  crctcshwlkn0lem5  26942  wspn0  27071  umgrwwlks2on  27105  elwspths2spth  27116  clwlkclwwlklem2a  27148  clwlkclwwlklem3  27151  clwwlkn1loopb  27199  clwlksfclwwlkOLD  27243  clwwlknonex2lem2  27284  3cyclfrgrrn2  27469  frgrncvvdeqlem8  27488  frgrwopregasn  27498  frgrwopregbsn  27499  frgrwopreg1  27500  frgrwopreg2  27501  frgrregord013  27594  frgrogt3nreg  27596  ablocom  27742  ubthlem1  28066  shaddcl  28414  shmulcl  28415  spansnss2  28774  cnopc  29112  cnfnc  29129  adj1  29132  pjorthcoi  29368  stj  29434  mdsl1i  29520  chirredlem1  29589  mdsymlem5  29606  cdj3lem2b  29636  slmdlema  30096  pconncn  31544  cvmlift2lem1  31622  ss2mcls  31803  dfon2lem6  32029  frrlem4  32120  nofv  32147  nolesgn2o  32161  nosupbnd1lem5  32195  nn0prpw  32655  waj-ax  32750  lukshef-ax2  32751  bj-alrim  33020  bj-nexdt  33024  sucneqond  33550  ptrecube  33742  poimirlem26  33768  poimirlem29  33771  heiborlem1  33942  rngodm1dm2  34063  rngoueqz  34071  zerdivemp1x  34078  isdrngo3  34090  0rngo  34158  pridl  34168  ispridlc  34201  isdmn3  34205  dmnnzd  34206  elrelscnveq3  34583  lshpcmp  34797  omllaw  35052  dochexmidlem7  37276  lspindp5  37580  dfac21  38162  eexinst11  39258  ax6e2eq  39298  e222  39386  e111  39424  e333  39485  imarnf1pr  41824  2ffzoeq  41866  iccpartigtl  41887  iccpartgt  41891  pfxccatin12lem2  41952  pfxccatin12  41953  pfxccat3  41954  lighneallem3  42052  lighneal  42056  evenltle  42154  sgoldbeven3prm  42199  bgoldbtbndlem2  42222  nrhmzr  42401  nzerooringczr  42600  gsumpr  42667  lincdifsn  42741  snlindsntor  42788  lincresunit3lem1  42796  lincresunit3lem2  42797  lincresunit3  42798  setrec1lem2  42963
  Copyright terms: Public domain W3C validator