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

Theorem syl5 34
Description: A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 25-May-2013.)
Hypotheses
Ref Expression
syl5.1 (𝜑𝜓)
syl5.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5 (𝜒 → (𝜑𝜃))

Proof of Theorem syl5
StepHypRef Expression
1 syl5.1 . . 3 (𝜑𝜓)
2 syl5.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5com 31 . 2 (𝜑 → (𝜒𝜃))
43com12 32 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:  syl56  36  syl2im  40  imim12i  62  pm2.86d  108  con2d  134  con3d  152  nsyli  157  biimtrid  241  biimtrrid  242  imbitrid  243  adantld  491  adantrd  492  impel  506  mpan9  507  pm4.72  948  pm2.36  968  pm4.79  1002  ecased  1033  ecase3adOLD  1035  alrimdh  1866  stdpc5v  1941  19.37imv  1951  ax12w  2129  ax13dgen2  2134  ax12v  2172  spsd  2180  nf5r  2187  axc4  2315  equs5eALT  2364  ax13lem1  2373  nfeqf  2380  hbae  2430  ax12vALT  2468  2ax6elem  2469  sb1  2478  euimmo  2617  necon2ad  2956  necon4ad  2960  r19.37v  3176  spcimgft  3544  rr19.28v  3618  moeq3  3668  reuimrmo  3701  sbeqalb  3805  csbexg  5265  ralxfrd  5361  ralxfrd2  5365  ralxfrALT  5368  copsexgw  5445  copsexg  5446  pwssun  5526  somo  5580  ssrel  5736  ssrelOLD  5737  relssres  5976  dmsnopg  6163  dfco2a  6196  dfpo2  6246  frpoinsg  6295  wfisgOLD  6306  tz7.7  6341  ordunidif  6364  suctr  6401  trsucss  6403  suc11  6421  imadif  6582  dffv2  6933  fvmptd3f  6960  fvmptnf  6967  foco2  7053  fconst5  7151  isores3  7276  riotaxfrd  7342  ovmpt4g  7496  ovmpos  7497  ov2gf  7498  ovmpodf  7505  sorpsscmpl  7663  abnexg  7682  onint  7717  limuni3  7780  tfisg  7782  tfis  7783  tfinds  7788  limomss  7799  peano5  7822  peano5OLD  7823  fo2ndf  8045  frxp  8050  xpord2pred  8069  xpord2indlem  8071  soseq  8083  suppss2  8123  suppssfv  8125  rntpos  8162  fprlem1  8223  fprresex  8233  wfr3g  8245  wfrlem5OLD  8251  wfrlem17OLD  8263  onfununi  8279  smofvon2  8294  smo11  8302  smoord  8303  tfrlem11  8326  tz7.44-2  8345  tz7.48lem  8379  tz7.48-1  8381  tz7.49  8383  tz7.49c  8384  omordi  8505  omord  8507  omass  8519  oneo  8520  omeulem1  8521  omopth2  8523  oewordri  8531  oeworde  8532  nnmordi  8570  nnmord  8571  omabs  8589  nnneo  8593  omsmo  8596  qsel  8693  eceqoveq  8719  domunsncan  8974  sucdom2OLD  8984  sbthlem1  8985  2pwuninel  9034  mapen  9043  infensuc  9057  rexdif1en  9060  findcard2  9066  pssnn  9070  ssfi  9075  sucdom2  9108  php  9112  onomeneq  9130  0sdom1dom  9140  sdom1  9144  pssnnOLD  9167  dif1ennnALT  9179  findcard2OLD  9186  ac6sfi  9189  frfi  9190  unblem1  9197  unblem2  9198  unbnn2  9202  nnsdomgOLD  9205  xpfiOLD  9220  domunfican  9222  fiint  9226  ixpfi2  9252  finsschain  9261  marypha1lem  9327  oiexg  9429  brwdom3  9476  inf3lem2  9523  inf3lem3  9524  cantnfval2  9563  cantnflt  9566  cantnflem1  9583  cnfcom  9594  ttrclss  9614  trcl  9622  epfrs  9625  frmin  9643  frinsg  9645  frr3g  9650  frrlem15  9651  r1sdom  9668  cardsdomel  9868  carduni  9875  pr2neOLD  9899  infpwfien  9956  carduniima  9990  dfac5  10022  dfac12r  10040  dfac12k  10041  kmlem11  10054  djuinf  10082  infxp  10109  cfsuc  10151  cfcoflem  10166  coftr  10167  infpssr  10202  fin23lem30  10236  isf32lem1  10247  isf34lem6  10274  fin1a2lem13  10306  fin1a2s  10308  axcc2lem  10330  domtriomlem  10336  axcclem  10351  ac6num  10373  zorn2lem5  10394  zorn2lem6  10395  axdclem2  10414  alephval2  10466  alephreg  10476  pwcfsdom  10477  axregndlem1  10496  axregnd  10498  axacndlem1  10501  axacndlem2  10502  axacndlem3  10503  axacndlem4  10504  axacnd  10506  gchi  10518  fpwwe2lem12  10536  canthp1  10548  gchpwdom  10564  wunfi  10615  tskwe2  10667  inar1  10669  gruen  10706  intgru  10708  indpi  10801  nqereu  10823  ltbtwnnq  10872  prnmadd  10891  genpcd  10900  prlem934  10927  ltexprlem1  10930  ltexprlem2  10931  ltexprlem7  10936  ltaprlem  10938  ltapr  10939  reclem4pr  10944  suplem2pr  10947  mulcmpblnr  10965  recexsrlem  10997  mulgt0sr  10999  supsrlem  11005  axpre-sup  11063  1re  11113  dedekindle  11277  addlsub  11529  recex  11745  nnunb  12367  0mnnnnn0  12403  prime  12542  zeo  12547  fnn0ind  12560  zindd  12562  btwnz  12564  lbzbi  12815  xrub  13185  elfznelfzo  13631  addmodlteq  13805  facwordi  14142  fiinfnf1o  14203  hashclb  14211  hashdom  14232  hashf1lem2  14308  seqcoll  14316  brfi1indALT  14352  ccatalpha  14434  pfxccatin12lem2a  14572  limsupbnd2  15324  rlimdm  15392  o1of2  15454  rlimno1  15497  isercoll  15511  caurcvg2  15521  caucvgb  15523  serf0  15524  zsum  15562  fsum2dlem  15614  fsum2d  15615  fsumabs  15645  fsumrlim  15655  fsumo1  15656  fsumiun  15665  zprod  15779  fprod2dlem  15822  fprod2d  15823  odd2np1  16182  ndvdssub  16250  dfgcd2  16386  nprm  16523  maxprmfct  16544  rpexp  16557  pc2dvds  16710  pcfac  16730  unbenlem  16739  4sqlem12  16787  4sqlem17  16792  vdwlem13  16824  prmlem0  16937  mreiincl  17435  sscfn1  17659  initoid  17846  termoid  17847  funcestrcsetclem8  17994  funcsetcestrclem8  18009  pospo  18193  cnvpsb  18427  dirtr  18450  mulgaddcom  18858  mulginvcom  18859  gaass  19035  cntz2ss  19071  elsymgbas  19113  symgfix2  19156  pmtrfrn  19198  psgnran  19255  odmulg  19296  odhash3  19316  sylow2alem1  19357  sylow2alem2  19358  pj1eu  19436  efgs1b  19476  efgsfo  19479  efgredlemc  19485  efgredeu  19492  frgpuptinv  19511  lt6abl  19630  ghmcyg  19631  ablfac1eulem  19809  pgpfac1lem5  19816  ablsimpgfindlem1  19844  ringinvnz1ne0  19968  irredmul  20090  acsfn1p  20218  lspextmo  20469  lspsncv0  20559  psgnghm  20936  mplcoe1  21389  mplcoe5  21392  evlseu  21444  mhpsclcl  21488  mdetunilem7  21918  mdetunilem9  21920  chcoeffeq  22186  cnindis  22594  lmss  22600  lmcls  22604  lmcnp  22606  hausnei  22630  cmpsub  22702  tgcmp  22703  fiuncmp  22706  cmpfi  22710  bwth  22712  1stcrest  22755  2ndcdisj  22758  1stccnp  22764  comppfsc  22834  1stckgenlem  22855  txcls  22906  txcn  22928  txlm  22950  tx1stc  22952  xkococn  22962  hmphdis  23098  ptcmpfi  23115  isfild  23160  fgss2  23176  filconn  23185  trfil2  23189  ufileu  23221  filufint  23222  elfm2  23250  flftg  23298  fclssscls  23320  fclscf  23327  ufilcmp  23334  cnpfcf  23343  alexsubb  23348  alexsubALTlem4  23352  alexsubALT  23353  qustgpopn  23422  tsmsxp  23457  isust  23506  xmettri2  23644  blin2  23733  setsmstopn  23784  met2ndc  23830  metcnp3  23847  tngtopn  23965  reconnlem2  24141  xrge0tsms  24148  fsumcn  24184  bndth  24272  iscmet3lem2  24607  iscmet3  24608  ivthlem1  24766  ivthlem2  24767  ivthlem3  24768  ovolfiniun  24816  volfiniun  24862  ioombl1lem4  24876  ismbf3d  24969  mbfi1flimlem  25038  itg2seq  25058  itgfsum  25142  ellimc3  25194  dvmptfsum  25290  c1liplem1  25311  plypf1  25524  plydivex  25608  aannenlem1  25639  ulmval  25690  ulmcau  25705  ulmbdd  25708  ulmcn  25709  ulmdvlem3  25712  sineq0  25831  efopn  25964  cxpeq  26061  logbgcd1irr  26095  rlimcnp  26266  xrlimcnp  26269  lgsdir2lem2  26625  lgsne0  26634  2lgsoddprm  26715  2sqlem6  26722  2sqlem10  26727  2sqreunnltblem  26750  sltval2  26955  noetasuplem4  27035  conway  27089  madebdayim  27167  axcontlem2  27742  uhgr0vb  27851  uvtx01vtx  28173  uvtxupgrres  28184  fusgrn0degnn0  28275  finsumvtxdg2size  28326  cusgrm1rusgr  28358  wlkv0  28427  wlklenvclwlk  28431  uspgrn2crct  28581  frrusgrord  29113  numclwwlk1lem2fo  29130  isgrpo  29267  grpoidinvlem3  29276  vcdi  29335  vcdir  29336  vcass  29337  nvs  29433  nvtri  29440  blocnilem  29574  chintcli  30101  hsupss  30111  shlej1  30130  elspansn4  30343  spansncvi  30422  hoaddsub  30586  lnopl  30684  lnfnl  30701  riesz4i  30833  pjnormssi  30938  pj3si  30977  stlei  31010  stcltr2i  31045  dmdmd  31070  dmdbr5  31078  mdslmd1lem2  31096  atssma  31148  atcvatlem  31155  chirredlem1  31160  atcvat4i  31167  mdsymlem2  31174  mdsymlem6  31178  sumdmdlem2  31189  cdjreui  31202  elimifd  31292  disjxpin  31333  unifi3  31453  xrge0infss  31489  xrge0tsmsd  31723  gsumle  31756  gsumvsca1  31885  gsumvsca2  31886  lmxrge0  32336  ismeas  32601  eulerpartlemb  32771  bnj849  33340  bnj1110  33397  srcmpltd  33489  swrdrevpfx  33513  cusgredgex2  33519  subgrwlk  33529  cusgr3cyclex  33533  umgr2cycllem  33537  umgr2cycl  33538  connpconn  33632  cvmseu  33673  cvmliftlem15  33695  cvmlift2lem1  33699  cvmlift2lem12  33711  satfv0fun  33768  satffunlem  33798  mclsind  33967  dfon2lem3  34169  dfon2lem4  34170  dfon2lem6  34172  dfon2lem8  34174  dfon2lem9  34175  hbntg  34189  naddcllem  34225  addsass  34303  cgrdegen  34520  funtransport  34547  ifscgr  34560  cgrxfr  34571  brofs2  34593  brifs2  34594  idinside  34600  btwnconn1lem7  34609  btwnconn1lem11  34613  btwnconn1lem12  34614  btwnconn1lem14  34616  broutsideof2  34638  btwnoutside  34641  outsideoftr  34645  finminlem  34721  ntruni  34730  neibastop1  34762  ontgval  34834  ordtop  34839  ordcmp  34850  onint1  34852  bj-ax12w  35072  axc11n11r  35079  bj-ax12v3  35081  bj-nnfan  35144  bj-nnfand  35145  bj-nnflemea  35161  bj-19.42t  35169  bj-sbft  35171  bj-hbaeb2  35214  bj-spcimdv  35293  bj-spcimdvv  35294  bj-sngltag  35385  bj-xtagex  35391  bj-0int  35503  bj-ismooredr  35511  bj-inftyexpiinj  35611  nlpfvineqsn  35811  wl-ax13lem1  35896  wl-speqv  35912  wl-sbcom2d  35947  wl-ax11-lem3  35970  wl-ax11-lem8  35975  tan2h  36001  ptrest  36008  poimirlem20  36029  poimirlem22  36031  poimirlem26  36035  poimirlem30  36039  poimirlem31  36040  poimirlem32  36041  heicant  36044  voliunnfl  36053  volsupnfl  36054  itg2addnclem2  36061  itg2addnc  36063  itg2gt0cn  36064  ftc2nc  36091  filbcmb  36130  sdclem2  36132  seqpo  36137  nninfnub  36141  neificl  36143  prdstotbnd  36184  cnpwstotbnd  36187  heibor1lem  36199  heibor  36211  bfplem2  36213  opidonOLD  36242  exidu1  36246  grpokerinj  36283  rngoideu  36293  rngodi  36294  rngodir  36295  rngmgmbs4  36321  divrngidl  36418  prnc  36457  eqvrelqsel  37009  erimeq2  37071  prter2  37274  ax4fromc4  37287  hbae-o  37296  dvelimf-o  37322  ax12indn  37336  ax12inda2  37340  ax12a2-o  37343  l1cvpat  37447  atcvrj0  37822  pmaple  38155  paddasslem5  38218  pclfinN  38294  osumcllem11N  38360  pexmidlem8N  38371  dvheveccl  39506  dihord6apre  39650  lpolconN  39881  lcmineqlem1  40417  oexpreposd  40709  sn-it0e0  40786  cnreeu  40839  isnacs3  40935  pellexlem5  41058  pellex  41060  jm2.18  41214  jm2.15nn0  41229  jm2.16nn0  41230  dford3lem2  41253  ttac  41262  onexomgt  41477  onexoegt  41480  omabs2  41565  omcl3g  41567  safesnsupfiss  41591  rp-isfinite5  41693  cnvssb  41762  clcnvlem  41799  iunrelexpuztr  41895  rfovcnvf1od  42180  ntrrn  42298  nzss  42501  pm11.71  42581  axc11next  42590  hbntal  42739  eel2122old  42904  fsetsnf1  45180  2reu8i  45239  afvelima  45293  rlimdmafv  45303  rlimdmafv2  45384  elsprel  45561  sfprmdvdsmersenne  45689  perfectALTVlem2  45808  fpprwppr  45825  copisnmnd  45997  rnghmsscmap2  46165  rnghmsscmap  46166  rhmsscmap2  46211  rhmsscmap  46212  funcringcsetcALTV2lem8  46235  funcringcsetclem8ALTV  46258  lindslinindsimp2lem5  46437  nn0sumshdig  46603  prelrrx2b  46694  itscnhlc0yqe  46739  iscnrm3lem2  46861  spd  47017  setrec1lem4  47029  setrec2fun  47031  aacllem  47142
  Copyright terms: Public domain W3C validator