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  1968  sbequ2OLD  2243  axc16i  2436  eupickbi  2638  ceqsalgALT  3477  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spcegv  3555  spc2egv  3557  disjne  4413  uneqdifeq  4449  preqsnd  4815  preq12nebg  4819  opthprneg  4821  dfiun2g  4989  pocl  5550  relresfld  6225  unixpid  6233  ordnbtwn  6407  sucssel  6409  ordelinel  6415  funmo  6512  fvimacnv  6999  2f1fvneq  7202  ordsuc  7739  ordsucOLD  7740  tfi  7780  focdmex  7879  f1ovv  7881  opreuopreu  7957  frrlem4  8188  wfrlem4OLD  8226  wfrlem10OLD  8232  tz7.49  8359  oeworde  8508  fsetprcnex  8734  dom2d  8867  findcard  9041  fisupg  9169  dffi3  9301  noinfep  9530  cantnflem2  9560  ttrcltr  9586  tcmin  9611  rankr1ag  9672  rankunb  9720  rankxpsuc  9752  alephordi  9944  alephsucdom  9949  alephinit  9965  dfac9  10006  ackbij2lem4  10112  cff1  10128  cfslbn  10137  cfcoflem  10142  cfcof  10144  infpssrlem5  10177  isfin7-2  10266  acncc  10310  domtriomlem  10312  axdc3lem2  10321  ttukeylem1  10379  iundom2g  10410  axpowndlem3  10469  wunex2  10608  grupr  10667  gruiun  10669  eltskm  10713  nqereu  10799  addcanpr  10916  axpre-sup  11039  relin01  11613  nneo  12521  zeo2  12524  xrub  13161  uznfz  13454  difelfzle  13484  ssfzo12  13595  facndiv  14117  hashgt12el2  14252  hash2prde  14298  hash2pwpr  14304  hashle2prv  14306  fi1uzind  14325  swrdswrd  14526  pfxccatin12lem2  14552  pfxccatin12  14554  pfxccat3  14555  cshwidxmod  14624  2cshwcshw  14647  fsumcom2  15595  fprodss  15767  fprodcom2  15803  sumodd  16206  ndvdssub  16227  eucalglt  16397  prmind2  16497  coprm  16523  prmdiveq  16594  prmdvdsprmop  16851  prmgaplem5  16863  cicsym  17623  drsdir  18127  lublecllem  18185  istos  18243  tsrlin  18410  dirge  18428  mhmlin  18545  issubg2  18878  nsgbi  18894  symgextf1lem  19137  sylow2a  19336  gsumpr  19667  issubrg2  20171  abvmul  20217  abvtri  20218  lmodlema  20256  rmodislmodlem  20318  rmodislmod  20319  rmodislmodOLD  20320  lspsnel6  20384  lmhmlin  20425  lbsind  20470  0ringnnzr  20668  0ring01eq  20670  01eq0ring  20671  ipcj  20967  obsip  21056  lindsss  21159  mamufacex  21666  mavmulsolcl  21828  slesolvec  21956  inopn  22176  basis1  22228  tgss  22246  tgcl  22247  elcls3  22362  neindisj2  22402  cncls  22553  1stcelcls  22740  qtoptop2  22978  nrmr0reg  23028  fbasssin  23115  fbfinnfr  23120  fbunfip  23148  filufint  23199  uffix  23200  ufinffr  23208  ufilen  23209  fmfnfmlem1  23233  flftg  23275  alexsubALT  23330  xmeteq0  23619  blssexps  23707  blssex  23708  mopni3  23778  neibl  23785  metss  23792  metcnp3  23824  nmvs  23968  iccntr  24112  reconnlem2  24118  lebnumlem3  24254  caubl  24600  bcthlem5  24620  ovolunlem1  24789  voliunlem1  24842  volsuplem  24847  ellimc3  25171  logbgcd1irr  26072  lgsqrmodndvds  26629  gausslemma2dlem0i  26640  2lgsoddprmlem3  26690  dchrisumlema  26764  nofv  26933  nolesgn2o  26947  nogesgn1o  26949  nosupbnd1lem5  26988  umgrnloopv  27862  usgrnloopvALT  27954  umgrres1lem  28063  upgrres1  28066  nbuhgr  28096  cplgrop  28190  fusgrregdegfi  28322  g0wlk0  28405  wlkdlem2  28436  upgrwlkdvdelem  28489  crctcshwlkn0lem3  28562  crctcshwlkn0lem5  28564  wspn0  28674  umgrwwlks2on  28707  elwspths2spth  28717  clwlkclwwlklem2a  28747  clwlkclwwlklem3  28750  clwwlkn1loopb  28792  clwwlknonwwlknonb  28855  clwwlknonex2lem2  28857  3cyclfrgrrn2  29036  frgrncvvdeqlem8  29055  frgrwopregasn  29065  frgrwopregbsn  29066  frgrwopreg1  29067  frgrwopreg2  29068  frgrregord013  29144  frgrogt3nreg  29146  ablocom  29295  ubthlem1  29617  shaddcl  29964  shmulcl  29965  spansnss2  30322  cnopc  30660  cnfnc  30677  adj1  30680  pjorthcoi  30916  stj  30982  mdsl1i  31068  chirredlem1  31137  mdsymlem5  31154  cdj3lem2b  31184  slmdlema  31839  isprmidlc  32016  pconncn  33598  cvmlift2lem1  33676  fmla0xp  33757  ss2mcls  33942  dfon2lem6  34157  addsprop  34284  negsprop  34321  waj-ax  34817  lukshef-ax2  34818  bj-alrim  35089  bj-nexdt  35093  sucneqond  35767  rdgssun  35780  ptrecube  36009  poimirlem26  36035  poimirlem29  36038  heiborlem1  36201  rngodm1dm2  36322  rngoueqz  36330  zerdivemp1x  36337  isdrngo3  36349  0rngo  36417  pridl  36427  ispridlc  36460  isdmn3  36464  dmnnzd  36465  elrelscnveq3  36884  lshpcmp  37381  omllaw  37636  dochexmidlem7  39860  lspindp5  40164  fsuppind  40667  dfac21  41295  eexinst11  42610  ax6e2eq  42640  e222  42719  e111  42757  e333  42816  natlocalincr  44906  tworepnotupword  44916  imarnf1pr  45305  2ffzoeq  45351  iccpartigtl  45406  iccpartgt  45410  lighneallem3  45590  lighneal  45594  requad1  45605  evenltle  45700  fppr2odd  45714  sgoldbeven3prm  45766  bgoldbtbndlem2  45789  isomuspgrlem2b  45812  nrhmzr  45962  nzerooringczr  46161  lincdifsn  46296  lindslinindimp2lem4  46333  snlindsntor  46343  lincresunit3lem1  46351  lincresunit3lem2  46352  f002  46711  setrec1lem2  46924
  Copyright terms: Public domain W3C validator