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  1874  axc11nlemOLD2  1986  axc11nlemOLD  2158  axc11nlemALT  2304  axc11nOLD  2306  axc11nOLDOLD  2307  axc11nALT  2308  axc16i  2320  eupickbi  2537  ceqsalgALT  3226  cgsexg  3233  cgsex2g  3234  cgsex4g  3235  spc2egv  3290  spc3egv  3292  disjne  4013  uneqdifeq  4048  uneqdifeqOLD  4049  relresfld  5650  unixpid  5658  ordnbtwn  5804  sucssel  5807  ordelinel  5813  fvimacnv  6318  2f1fvneq  6502  ordsuc  6999  tfi  7038  fornex  7120  f1ovv  7122  wfrlem4  7403  wfrlem10  7409  tz7.49  7525  oeworde  7658  dom2d  7981  findcard  8184  fisupg  8193  dffi3  8322  fiinfg  8390  noinfep  8542  cantnflem2  8572  tcmin  8602  rankr1ag  8650  rankelb  8672  rankunb  8698  rankxpsuc  8730  alephordi  8882  alephsucdom  8887  alephinit  8903  dfac9  8943  ackbij2lem4  9049  cff1  9065  cfslbn  9074  cfcoflem  9079  cfcof  9081  infpssrlem5  9114  isfin7-2  9203  acncc  9247  domtriomlem  9249  axdc3lem2  9258  ttukeylem1  9316  iundom2g  9347  axpowndlem3  9406  wunex2  9545  grupr  9604  gruiun  9606  eltskm  9650  nqereu  9736  addcanpr  9853  axpre-sup  9975  relin01  10537  nneo  11446  zeo2  11449  xrub  12127  uznfz  12407  difelfzle  12436  ssfzo12  12545  facndiv  13058  hashf1rnOLD  13126  hashgt12el2  13194  hash2prde  13235  hash2pwpr  13241  hashle2prv  13243  fi1uzind  13262  fi1uzindOLD  13268  swrdswrd  13442  swrdccatin2  13468  swrdccatin12lem2  13470  swrdccatin12  13472  swrdccat3  13473  swrdccatid  13478  repswswrd  13512  2cshwcshw  13552  relexpcnvd  13757  relexpdmd  13765  relexprnd  13769  relexpfldd  13771  relexpaddd  13775  fsumcom2  14486  fsumcom2OLD  14487  fprodss  14659  fprodcom2  14695  fprodcom2OLD  14696  sumodd  15092  ndvdssub  15114  eucalglt  15279  prmind2  15379  coprm  15404  prmdiveq  15472  prmdvdsprmop  15728  prmgaplem5  15740  drsdir  16916  lublecllem  16969  istos  17016  tsrlin  17200  dirge  17218  mhmlin  17323  issubg2  17590  nsgbi  17606  symgextf1lem  17821  sylow2a  18015  issubrg2  18781  abvmul  18810  abvtri  18811  lmodlema  18849  rmodislmodlem  18911  rmodislmod  18912  lspsnel6  18975  lmhmlin  19016  lbsind  19061  0ring01eq  19252  01eq0ring  19253  gsummoncoe1  19655  ipcj  19960  obsip  20046  lindsss  20144  mamufacex  20176  mavmulsolcl  20338  slesolvec  20466  inopn  20685  basis1  20735  tgss  20753  tgcl  20754  elcls3  20868  neindisj2  20908  cncls  21059  1stcelcls  21245  qtoptop2  21483  nrmr0reg  21533  fbasssin  21621  fbfinnfr  21626  fbunfip  21654  filufint  21705  uffix  21706  ufinffr  21714  ufilen  21715  fmfnfmlem1  21739  flftg  21781  alexsubALT  21836  xmeteq0  22124  blssexps  22212  blssex  22213  mopni3  22280  neibl  22287  metss  22294  metcnp3  22326  nmvs  22461  reperflem  22602  iccntr  22605  reconnlem2  22611  lebnumlem3  22743  caubl  23087  bcthlem5  23106  ovolunlem1  23246  voliunlem1  23299  volsuplem  23304  ellimc3  23624  lhop1lem  23757  ulmss  24132  2lgsoddprmlem3  25120  dchrisumlema  25158  umgrnloopv  25982  usgrnloopvALT  26074  umgrres1lem  26183  upgrres1  26186  nbuhgr  26220  cplgrop  26314  fusgrregdegfi  26446  g0wlk0  26529  wlkdlem2  26561  upgrwlkdvdelem  26613  crctcshwlkn0lem4  26686  crctcshwlkn0lem5  26687  umgrwwlks2on  26831  elwspths2spth  26843  clwlkclwwlklem2a  26880  clwlkclwwlklem3  26883  clwlksfclwwlk  26942  3cyclfrgrrn2  27131  frgrncvvdeqlem8  27150  frgrwopreg1  27160  frgrwopreg2  27161  numclwwlkovf2ex  27191  frgrregord013  27223  frgrogt3nreg  27225  ablocom  27372  ubthlem1  27696  shaddcl  28044  shmulcl  28045  spansnss2  28404  cnopc  28742  cnfnc  28759  adj1  28762  pjorthcoi  28998  stj  29064  mdsl1i  29150  chirredlem1  29219  mdsymlem5  29236  cdj3lem2b  29266  slmdlema  29730  pconncn  31180  cvmlift2lem1  31258  ss2mcls  31439  dfon2lem6  31667  frrlem4  31757  nofv  31784  nolesgn2o  31798  nosupbnd1lem5  31832  nn0prpw  32293  waj-ax  32388  lukshef-ax2  32389  bj-alrim  32658  bj-nexdt  32662  sucneqond  33184  ptrecube  33380  poimirlem26  33406  poimirlem29  33409  heiborlem1  33581  rngodm1dm2  33702  rngoueqz  33710  zerdivemp1x  33717  isdrngo3  33729  0rngo  33797  pridl  33807  ispridlc  33840  isdmn3  33844  dmnnzd  33845  lshpcmp  34094  omllaw  34349  dochexmidlem7  36574  lspindp5  36878  dfac21  37455  eexinst11  38553  ax6e2eq  38593  e222  38681  e111  38719  e333  38780  imarnf1pr  41064  2ffzoeq  41101  iccpartigtl  41123  iccpartgt  41127  pfxccatin12lem2  41189  pfxccatin12  41190  pfxccat3  41191  lighneallem3  41289  lighneal  41293  evenltle  41391  sgoldbeven3prm  41436  bgoldbtbndlem2  41459  nrhmzr  41638  nzerooringczr  41837  gsumpr  41904  lincdifsn  41978  snlindsntor  42025  lincresunit3lem1  42033  lincresunit3lem2  42034  lincresunit3  42035  setrec1lem2  42200
  Copyright terms: Public domain W3C validator