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  peirceroll  85  pm2.86d  107  con2d  129  con3d  148  nsyli  155  syl5bi  232  syl5bir  233  syl5ib  234  adantld  484  adantrd  485  impel  486  mpan9  487  pm4.79  608  pm2.36  924  pm4.72  956  ecased  1022  ecase3ad  1023  syl3an2OLD  1169  syl2an23anOLD  1535  19.38a  1916  19.38b  1917  alrimdh  1939  stdpc5v  2016  19.37imv  2024  ax12w  2159  ax13dgen2  2164  ax12v  2197  spsd  2204  nf5r  2211  axc4  2277  equs5eALT  2323  ax13lem1  2393  nfeqf  2446  hbae  2457  ax12vALT  2565  2ax6elem  2586  euimmo  2660  necon2ad  2947  necon4ad  2951  spcimgft  3424  rr19.28v  3486  moeq3  3524  sbeqalb  3629  csbexg  4944  reusv2lem2OLD  5019  ralxfrd  5028  ralxfrdOLD  5029  ralxfrd2  5033  ralxfrALT  5036  copsexg  5104  pwssun  5170  somo  5221  ssrel  5364  relssres  5595  issref  5667  dmsnopg  5765  dfco2a  5796  wfisg  5876  tz7.7  5910  ordunidif  5934  suctr  5969  trsucss  5972  suc11  5992  imadif  6134  fvelima  6410  dffv2  6433  fvmptd3f  6457  fvmptf  6463  fvmptnf  6464  foco2  6542  foco2OLD  6543  fconst5  6635  funfvima2  6656  funfvima3  6658  isores3  6748  riotaxfrd  6805  ovmpt4g  6948  ovmpt2s  6949  ov2gf  6950  ovmpt2df  6957  sorpsscmpl  7113  abnexg  7129  onint  7160  limuni3  7217  tfi  7218  tfis  7219  tfinds  7224  limomss  7235  peano5  7254  fo2ndf  7452  frxp  7455  suppssov1  7496  suppss2  7498  suppssfv  7500  rntpos  7534  tposf2  7545  wfr3g  7582  wfrlem4  7587  wfrlem5  7588  wfrlem17  7600  onfununi  7607  smofvon2  7622  smo11  7630  smoord  7631  tfrlem11  7653  tz7.44-2  7672  tz7.48lem  7705  tz7.48-1  7707  tz7.49  7709  tz7.49c  7710  omordi  7815  omord  7817  omass  7829  oneo  7830  omeulem1  7831  omopth2  7833  oewordri  7841  oeworde  7842  nnmordi  7880  nnmord  7881  omabs  7896  nnneo  7900  omsmo  7903  qsel  7993  eceqoveq  8019  mapsn  8065  f1oeng  8140  domunsncan  8225  sbthlem1  8235  2pwuninel  8280  mapen  8289  infensuc  8303  nneneq  8308  sucdom2  8321  pssnn  8343  dif1en  8358  findcard2  8365  ac6sfi  8369  frfi  8370  unblem1  8377  unblem2  8378  unbnn2  8382  nnsdomg  8384  xpfi  8396  domunfican  8398  fiint  8402  fodomfi  8404  ixpfi2  8429  finsschain  8438  marypha1lem  8504  oiexg  8605  brwdom3  8652  inf3lem2  8699  inf3lem3  8700  cantnfval2  8739  cantnflt  8742  cantnflem1  8759  cantnf  8763  cnfcom  8770  trcl  8777  epfrs  8780  r1sdom  8810  rankwflemb  8829  rankelb  8860  carden2a  8982  cardsdomel  8990  carduni  8997  harval2  9013  pr2ne  9018  infpwfien  9075  cardaleph  9102  carduniima  9109  alephval3  9123  dfac5  9141  dfac12r  9160  dfac12k  9161  kmlem11  9174  cdainf  9206  infxp  9229  cfsuc  9271  cfcoflem  9286  coftr  9287  cfcof  9288  infpssr  9322  fin23lem30  9356  isf32lem1  9367  isf34lem6  9394  fin1a2lem13  9426  fin1a2s  9428  axcc2lem  9450  domtriomlem  9456  axdc4lem  9469  axcclem  9471  ac6num  9493  zorn2lem5  9514  zorn2lem6  9515  axdclem2  9534  alephval2  9586  alephreg  9596  pwcfsdom  9597  axregndlem1  9616  axregnd  9618  axacndlem1  9621  axacndlem2  9622  axacndlem3  9623  axacndlem4  9624  axacnd  9626  gchi  9638  fpwwe2lem13  9656  canthp1  9668  gchpwdom  9684  wunfi  9735  tskwe2  9787  inar1  9789  gruen  9826  intgru  9828  indpi  9921  nqereu  9943  ltbtwnnq  9992  prnmadd  10011  genpcd  10020  prlem934  10047  ltexprlem1  10050  ltexprlem2  10051  ltexprlem7  10056  ltaprlem  10058  ltapr  10059  reclem4pr  10064  suplem2pr  10067  mulcmpblnr  10084  recexsrlem  10116  mulgt0sr  10118  recexsr  10120  supsrlem  10124  axpre-sup  10182  1re  10231  dedekindle  10393  addlsub  10639  recex  10851  nnunb  11480  0mnnnnn0  11517  prime  11650  zeo  11655  fnn0ind  11668  zindd  11670  btwnz  11671  lbzbi  11969  xrub  12335  elfznelfzo  12767  addmodlteq  12939  facwordi  13270  fiinfnf1o  13332  hashclb  13341  hashdom  13360  hashf1lem2  13432  seqcoll  13440  brfi1indALT  13474  ccatalpha  13565  swrdccatin12lem2a  13685  limsupbnd2  14413  rlimdm  14481  o1of2  14542  rlimno1  14583  isercoll  14597  climcau  14600  caurcvg2  14607  caucvgb  14609  serf0  14610  zsum  14648  fsum2dlem  14700  fsum2d  14701  fsumabs  14732  fsumrlim  14742  fsumo1  14743  fsumiun  14752  zprod  14866  fprod2dlem  14909  fprod2d  14910  odd2np1  15267  ndvdssub  15335  dfgcd2  15465  coprmproddvdslem  15578  nprm  15603  maxprmfct  15623  rpexp  15634  pc2dvds  15785  pcfac  15805  unbenlem  15814  4sqlem12  15862  4sqlem17  15867  vdwlem6  15892  vdwlem13  15899  prmlem0  16014  xpscfv  16424  mreiincl  16458  sscfn1  16678  initoid  16856  termoid  16857  funcestrcsetclem8  16988  funcsetcestrclem8  17003  pospo  17174  cnvpsb  17414  dirref  17436  dirtr  17437  mulgaddcom  17765  mulginvcom  17766  gaass  17930  cntz2ss  17965  elsymgbas  18002  symgfix2  18036  pmtrfrn  18078  psgnran  18135  odmulg  18173  odhash3  18191  sylow2alem1  18232  sylow2alem2  18233  pj1eu  18309  efgs1b  18349  efgsfo  18352  efgredlemc  18358  efgredeu  18365  frgpuptinv  18384  lt6abl  18496  ghmcyg  18497  ablfac1eulem  18671  pgpfac1lem5  18678  ringinvnz1ne0  18792  irredn1  18906  irredmul  18909  lspextmo  19258  lspsncv0  19348  mplcoe1  19667  mplcoe5  19670  evlseu  19718  psgnghm  20128  mdetunilem7  20626  mdetunilem9  20628  chcoeffeq  20893  cnindis  21298  lmss  21304  lmcls  21308  lmcnp  21310  hausnei  21334  cmpsub  21405  tgcmp  21406  fiuncmp  21409  cmpfi  21413  bwth  21415  1stcrest  21458  2ndcdisj  21461  1stccnp  21467  comppfsc  21537  1stckgenlem  21558  txcls  21609  txcn  21631  txlm  21653  tx1stc  21655  xkococn  21665  hmphdis  21801  ptcmpfi  21818  isfild  21863  fgss2  21879  filconn  21888  trfil2  21892  ufileu  21924  filufint  21925  elfm2  21953  flftg  22001  fclssscls  22023  fclscf  22030  ufilcmp  22037  cnpfcf  22046  alexsubb  22051  alexsubALTlem4  22055  alexsubALT  22056  cnextcn  22072  qustgpopn  22124  tsmsxp  22159  isust  22208  xmettri2  22346  blin2  22435  setsmstopn  22484  met2ndc  22529  metcnp3  22546  tngtopn  22655  reconnlem2  22831  xrge0tsms  22838  fsumcn  22874  bndth  22958  iscmet3lem2  23290  iscmet3  23291  ivthlem1  23420  ivthlem2  23421  ivthlem3  23422  ovolfiniun  23469  volfiniun  23515  ioombl1lem4  23529  dyadmbl  23568  ismbf3d  23620  itg1addlem4  23665  mbfi1flimlem  23688  itg2seq  23708  itgfsum  23792  ellimc3  23842  dvmptfsum  23937  c1liplem1  23958  plypf1  24167  plydivex  24251  aannenlem1  24282  ulmval  24333  ulmcau  24348  ulmss  24350  ulmbdd  24351  ulmcn  24352  ulmdvlem3  24355  pserulm  24375  sineq0  24472  efopn  24603  cxpeq  24697  rlimcnp  24891  xrlimcnp  24894  perfectlem2  25154  lgsdir2lem2  25250  lgsne0  25259  2lgsoddprm  25340  2sqlem6  25347  2sqlem10  25352  dchrisumlem2  25378  axlowdimlem16  26036  axcontlem2  26044  uhgr0vb  26166  uvtx01vtx  26500  uvtxa01vtx0OLD  26502  uvtxupgrres  26513  fusgrn0degnn0  26605  finsumvtxdg2size  26656  cusgrm1rusgr  26688  wlkv0  26757  uspgrn2crct  26911  frrusgrord  27495  numclwlk1lem2fo  27517  isgrpo  27660  grpoidinvlem3  27669  vcdi  27729  vcdir  27730  vcass  27731  nvs  27827  nvtri  27834  blocnilem  27968  chintcli  28499  hsupss  28509  shlej1  28528  elspansn4  28741  spansncvi  28820  hoaddsub  28984  lnopl  29082  lnfnl  29099  riesz4i  29231  pjnormssi  29336  pj3si  29375  stlei  29408  stcltr2i  29443  dmdmd  29468  dmdbr5  29476  mdslmd1lem2  29494  atssma  29546  atcvatlem  29553  chirredlem1  29558  atcvat4i  29565  mdsymlem2  29572  mdsymlem6  29576  sumdmdlem2  29587  cdjreui  29600  elimifd  29669  disjxpin  29708  unifi3  29799  xrge0infss  29834  gsumle  30088  gsumvsca1  30091  gsumvsca2  30092  xrge0tsmsd  30094  lmxrge0  30307  ismeas  30571  eulerpartlemb  30739  bnj849  31302  bnj1110  31357  connpconn  31524  cvmseu  31565  cvmliftlem15  31587  cvmlift2lem1  31591  cvmlift2lem12  31603  mclsind  31774  dfpo2  31952  fundmpss  31971  dfon2lem3  31995  dfon2lem4  31996  dfon2lem6  31998  dfon2lem8  32000  dfon2lem9  32001  hbntg  32016  tfisg  32021  dftrpred3g  32038  trpredrec  32043  frpoinsg  32047  frinsg  32051  soseq  32060  frr3g  32085  frrlem5  32090  sltval2  32115  noetalem3  32171  conway  32216  cgrdegen  32417  funtransport  32444  ifscgr  32457  cgrxfr  32468  brofs2  32490  brifs2  32491  idinside  32497  btwnconn1lem7  32506  btwnconn1lem11  32510  btwnconn1lem12  32511  btwnconn1lem14  32513  broutsideof2  32535  btwnoutside  32538  outsideoftr  32542  finminlem  32618  ntruni  32628  neibastop1  32660  ontgval  32736  ordtop  32741  ordcmp  32752  onint1  32754  bj-ax12w  32971  axc11n11r  32979  bj-ax12v3  32981  bj-hbaeb2  33111  bj-spcimdv  33190  bj-spcimdvv  33191  bj-sngltag  33277  bj-xtagex  33283  bj-0int  33361  bj-ismooredr  33370  bj-inftyexpiinj  33407  wl-ax13lem1  33600  wl-speqv  33621  wl-sbcom2d  33657  wl-ax11-lem3  33677  wl-ax11-lem8  33682  tan2h  33714  ptrest  33721  poimirlem20  33742  poimirlem22  33744  poimirlem26  33748  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  heicant  33757  voliunnfl  33766  volsupnfl  33767  itg2addnclem2  33775  itg2addnc  33777  itg2gt0cn  33778  ftc2nc  33807  filbcmb  33848  sdclem2  33851  seqpo  33856  nninfnub  33860  neificl  33862  prdstotbnd  33906  cnpwstotbnd  33909  heibor1lem  33921  heibor  33933  bfplem2  33935  opidonOLD  33964  exidu1  33968  grpokerinj  34005  rngoideu  34015  rngodi  34016  rngodir  34017  rngmgmbs4  34043  divrngidl  34140  prnc  34179  prter2  34670  ax4fromc4  34683  hbae-o  34692  dvelimf-o  34718  ax12indn  34732  ax12inda2  34736  ax12a2-o  34739  l1cvpat  34844  atcvrj0  35217  pmaple  35550  paddasslem5  35613  pclfinN  35689  osumcllem11N  35755  pexmidlem8N  35766  dvheveccl  36903  dihord6apre  37047  lpolconN  37278  isnacs3  37775  pellexlem5  37899  pellex  37901  jm2.18  38057  jm2.15nn0  38072  jm2.16nn0  38073  dford3lem2  38096  ttac  38105  acsfn1p  38271  rp-isfinite5  38365  cnvssb  38394  clcnvlem  38432  iunrelexpuztr  38513  rfovcnvf1od  38800  ntrrn  38922  nzss  39018  pm11.71  39099  axc11next  39109  hbntal  39271  eel2122old  39445  mapsnd  39887  reuimrmo  41684  afvelima  41753  rlimdmafv  41763  sfprmdvdsmersenne  42030  perfectALTVlem2  42141  elsprel  42235  copisnmnd  42319  rnghmsscmap2  42483  rnghmsscmap  42484  rhmsscmap2  42529  rhmsscmap  42530  funcringcsetcALTV2lem8  42553  funcringcsetclem8ALTV  42576  lindslinindsimp2lem5  42761  nn0sumshdig  42927  spd  42935  setrec1lem4  42947  setrec2fun  42949  aacllem  43060
  Copyright terms: Public domain W3C validator