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  108  con2d  131  con3d  149  nsyli  156  syl5bi  233  syl5bir  234  syl5ib  235  adantld  480  adantrd  481  impel  497  mpan9  498  pm4.72  963  pm2.36  983  pm4.79  1017  ecased  1049  ecase3ad  1050  syl3an2OLD  1197  syl2an23anOLD  1540  19.38a  1924  19.38aOLD  1925  19.38b  1926  19.38bOLD  1927  alrimdh  1951  stdpc5v  2030  19.37imv  2038  ax12w  2176  ax13dgen2  2181  ax12v  2215  spsd  2222  nf5r  2229  axc4  2306  equs5eALT  2352  ax13lem1  2422  nfeqf  2469  hbae  2479  ax12vALT  2587  2ax6elem  2609  euimmo  2686  necon2ad  2993  necon4ad  2997  spcimgft  3477  rr19.28v  3541  moeq3  3581  sbeqalb  3686  csbexg  4987  ralxfrd  5077  ralxfrd2  5081  ralxfrALT  5084  copsexg  5145  pwssun  5215  somo  5266  ssrel  5409  relssres  5641  idrefOLD  5720  dmsnopg  5818  dfco2a  5849  wfisg  5928  tz7.7  5962  ordunidif  5986  suctr  6021  trsucss  6024  suc11  6044  imadif  6184  fvelima  6469  dffv2  6492  fvmptd3f  6516  fvmptf  6522  fvmptnf  6523  foco2  6601  fconst5  6696  funfvima2  6718  funfvima3  6720  isores3  6809  riotaxfrd  6866  ovmpt4g  7013  ovmpt2s  7014  ov2gf  7015  ovmpt2df  7022  sorpsscmpl  7178  abnexg  7194  onint  7225  limuni3  7282  tfi  7283  tfis  7284  tfinds  7289  limomss  7300  peano5  7319  fo2ndf  7518  frxp  7521  suppssov1  7562  suppss2  7564  suppssfv  7566  rntpos  7600  tposf2  7611  wfr3g  7648  wfrlem4OLD  7654  wfrlem5  7655  wfrlem17  7667  onfununi  7674  smofvon2  7689  smo11  7697  smoord  7698  tfrlem11  7720  tz7.44-2  7739  tz7.48lem  7772  tz7.48-1  7774  tz7.49  7776  tz7.49c  7777  omordi  7883  omord  7885  omass  7897  oneo  7898  omeulem1  7899  omopth2  7901  oewordri  7909  oeworde  7910  nnmordi  7948  nnmord  7949  omabs  7964  nnneo  7968  omsmo  7971  qsel  8061  eceqoveq  8088  mapsnd  8134  f1oeng  8211  domunsncan  8299  sbthlem1  8309  2pwuninel  8354  mapen  8363  infensuc  8377  nneneq  8382  sucdom2  8395  pssnn  8417  dif1en  8432  findcard2  8439  ac6sfi  8443  frfi  8444  unblem1  8451  unblem2  8452  unbnn2  8456  nnsdomg  8458  xpfi  8470  domunfican  8472  fiint  8476  fodomfi  8478  ixpfi2  8503  finsschain  8512  marypha1lem  8578  oiexg  8679  brwdom3  8726  inf3lem2  8773  inf3lem3  8774  cantnfval2  8813  cantnflt  8816  cantnflem1  8833  cantnf  8837  cnfcom  8844  trcl  8851  epfrs  8854  r1sdom  8884  rankwflemb  8903  rankelb  8934  carden2a  9075  cardsdomel  9083  carduni  9090  harval2  9106  pr2ne  9111  infpwfien  9168  cardaleph  9195  carduniima  9202  alephval3  9216  dfac5  9234  dfac12r  9253  dfac12k  9254  kmlem11  9267  cdainf  9299  infxp  9322  cfsuc  9364  cfcoflem  9379  coftr  9380  cfcof  9381  infpssr  9415  fin23lem30  9449  isf32lem1  9460  isf34lem6  9487  fin1a2lem13  9519  fin1a2s  9521  axcc2lem  9543  domtriomlem  9549  axdc4lem  9562  axcclem  9564  ac6num  9586  zorn2lem5  9607  zorn2lem6  9608  axdclem2  9627  alephval2  9679  alephreg  9689  pwcfsdom  9690  axregndlem1  9709  axregnd  9711  axacndlem1  9714  axacndlem2  9715  axacndlem3  9716  axacndlem4  9717  axacnd  9719  gchi  9731  fpwwe2lem13  9749  canthp1  9761  gchpwdom  9777  wunfi  9828  tskwe2  9880  inar1  9882  gruen  9919  intgru  9921  indpi  10014  nqereu  10036  ltbtwnnq  10085  prnmadd  10104  genpcd  10113  prlem934  10140  ltexprlem1  10143  ltexprlem2  10144  ltexprlem7  10149  ltaprlem  10151  ltapr  10152  reclem4pr  10157  suplem2pr  10160  mulcmpblnr  10177  recexsrlem  10209  mulgt0sr  10211  recexsr  10213  supsrlem  10217  axpre-sup  10275  1re  10325  dedekindle  10486  addlsub  10732  recex  10944  nnunb  11555  0mnnnnn0  11591  prime  11724  zeo  11729  fnn0ind  11742  zindd  11744  btwnz  11745  lbzbi  11995  xrub  12360  elfznelfzo  12797  addmodlteq  12969  facwordi  13296  fiinfnf1o  13358  hashclb  13367  hashdom  13386  hashf1lem2  13457  seqcoll  13465  brfi1indALT  13499  ccatalpha  13590  swrdccatin12lem2a  13709  limsupbnd2  14437  rlimdm  14505  o1of2  14566  rlimno1  14607  isercoll  14621  climcau  14624  caurcvg2  14631  caucvgb  14633  serf0  14634  zsum  14672  fsum2dlem  14724  fsum2d  14725  fsumabs  14755  fsumrlim  14765  fsumo1  14766  fsumiun  14775  zprod  14888  fprod2dlem  14931  fprod2d  14932  odd2np1  15285  ndvdssub  15352  dfgcd2  15482  coprmproddvdslem  15594  nprm  15619  maxprmfct  15638  rpexp  15649  pc2dvds  15800  pcfac  15820  unbenlem  15829  4sqlem12  15877  4sqlem17  15882  vdwlem6  15907  vdwlem13  15914  prmlem0  16024  xpscfv  16427  mreiincl  16461  sscfn1  16681  initoid  16859  termoid  16860  funcestrcsetclem8  16992  funcsetcestrclem8  17007  pospo  17178  cnvpsb  17418  dirref  17440  dirtr  17441  mulgaddcom  17768  mulginvcom  17769  gaass  17931  cntz2ss  17966  elsymgbas  18003  symgfix2  18037  pmtrfrn  18079  psgnran  18136  odmulg  18174  odhash3  18192  sylow2alem1  18233  sylow2alem2  18234  pj1eu  18310  efgs1b  18350  efgsfo  18353  efgredlemc  18359  efgredeu  18366  frgpuptinv  18385  lt6abl  18497  ghmcyg  18498  ablfac1eulem  18673  pgpfac1lem5  18680  ringinvnz1ne0  18794  irredn1  18908  irredmul  18911  lspextmo  19263  lspsncv0  19354  lspsncv0OLD  19355  mplcoe1  19674  mplcoe5  19677  evlseu  19724  psgnghm  20133  mdetunilem7  20635  mdetunilem9  20637  chcoeffeq  20904  cnindis  21310  lmss  21316  lmcls  21320  lmcnp  21322  hausnei  21346  cmpsub  21417  tgcmp  21418  fiuncmp  21421  cmpfi  21425  bwth  21427  1stcrest  21470  2ndcdisj  21473  1stccnp  21479  comppfsc  21549  1stckgenlem  21570  txcls  21621  txcn  21643  txlm  21665  tx1stc  21667  xkococn  21677  hmphdis  21813  ptcmpfi  21830  isfild  21875  fgss2  21891  filconn  21900  trfil2  21904  ufileu  21936  filufint  21937  elfm2  21965  flftg  22013  fclssscls  22035  fclscf  22042  ufilcmp  22049  cnpfcf  22058  alexsubb  22063  alexsubALTlem4  22067  alexsubALT  22068  cnextcn  22084  qustgpopn  22136  tsmsxp  22171  isust  22220  xmettri2  22358  blin2  22447  setsmstopn  22496  met2ndc  22541  metcnp3  22558  tngtopn  22667  reconnlem2  22843  xrge0tsms  22850  fsumcn  22886  bndth  22970  iscmet3lem2  23302  iscmet3  23303  ivthlem1  23432  ivthlem2  23433  ivthlem3  23434  ovolfiniun  23482  volfiniun  23528  ioombl1lem4  23542  dyadmbl  23581  ismbf3d  23635  itg1addlem4  23680  mbfi1flimlem  23703  itg2seq  23723  itgfsum  23807  ellimc3  23857  dvmptfsum  23952  c1liplem1  23973  plypf1  24182  plydivex  24266  aannenlem1  24297  ulmval  24348  ulmcau  24363  ulmss  24365  ulmbdd  24366  ulmcn  24367  ulmdvlem3  24370  pserulm  24390  sineq0  24488  efopn  24618  cxpeq  24712  rlimcnp  24906  xrlimcnp  24909  perfectlem2  25169  lgsdir2lem2  25265  lgsne0  25274  2lgsoddprm  25355  2sqlem6  25362  2sqlem10  25367  dchrisumlem2  25393  axlowdimlem16  26051  axcontlem2  26059  uhgr0vb  26181  uvtx01vtx  26518  uvtxa01vtx0OLD  26520  uvtxupgrres  26531  fusgrn0degnn0  26623  finsumvtxdg2size  26674  cusgrm1rusgr  26706  wlkv0  26775  uspgrn2crct  26929  frrusgrord  27516  numclwwlk1lem2fo  27537  isgrpo  27680  grpoidinvlem3  27689  vcdi  27748  vcdir  27749  vcass  27750  nvs  27846  nvtri  27853  blocnilem  27987  chintcli  28518  hsupss  28528  shlej1  28547  elspansn4  28760  spansncvi  28839  hoaddsub  29003  lnopl  29101  lnfnl  29118  riesz4i  29250  pjnormssi  29355  pj3si  29394  stlei  29427  stcltr2i  29462  dmdmd  29487  dmdbr5  29495  mdslmd1lem2  29513  atssma  29565  atcvatlem  29572  chirredlem1  29577  atcvat4i  29584  mdsymlem2  29591  mdsymlem6  29595  sumdmdlem2  29606  cdjreui  29619  elimifd  29687  disjxpin  29726  unifi3  29817  xrge0infss  29852  gsumle  30104  gsumvsca1  30107  gsumvsca2  30108  xrge0tsmsd  30110  lmxrge0  30323  ismeas  30587  eulerpartlemb  30755  bnj849  31318  bnj1110  31373  connpconn  31540  cvmseu  31581  cvmliftlem15  31603  cvmlift2lem1  31607  cvmlift2lem12  31619  mclsind  31790  dfpo2  31967  fundmpss  31986  dfon2lem3  32010  dfon2lem4  32011  dfon2lem6  32013  dfon2lem8  32015  dfon2lem9  32016  hbntg  32031  tfisg  32036  dftrpred3g  32053  trpredrec  32058  frpoinsg  32062  frinsg  32066  soseq  32075  frr3g  32100  frrlem5  32105  sltval2  32130  noetalem3  32186  conway  32231  cgrdegen  32432  funtransport  32459  ifscgr  32472  cgrxfr  32483  brofs2  32505  brifs2  32506  idinside  32512  btwnconn1lem7  32521  btwnconn1lem11  32525  btwnconn1lem12  32526  btwnconn1lem14  32528  broutsideof2  32550  btwnoutside  32553  outsideoftr  32557  finminlem  32633  ntruni  32643  neibastop1  32675  ontgval  32747  ordtop  32752  ordcmp  32763  onint1  32765  bj-ax12w  32980  axc11n11r  32988  bj-ax12v3  32990  bj-hbaeb2  33118  bj-spcimdv  33192  bj-spcimdvv  33193  bj-sngltag  33281  bj-xtagex  33287  bj-0int  33366  bj-ismooredr  33375  bj-inftyexpiinj  33413  wl-ax13lem1  33605  wl-speqv  33623  wl-sbcom2d  33658  wl-ax11-lem3  33678  wl-ax11-lem8  33683  tan2h  33714  ptrest  33721  poimirlem20  33742  poimirlem22  33744  poimirlem26  33748  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  heicant  33757  voliunnfl  33766  volsupnfl  33767  itg2addnclem2  33774  itg2addnc  33776  itg2gt0cn  33777  ftc2nc  33806  filbcmb  33847  sdclem2  33849  seqpo  33854  nninfnub  33858  neificl  33860  prdstotbnd  33904  cnpwstotbnd  33907  heibor1lem  33919  heibor  33931  bfplem2  33933  opidonOLD  33962  exidu1  33966  grpokerinj  34003  rngoideu  34013  rngodi  34014  rngodir  34015  rngmgmbs4  34041  divrngidl  34138  prnc  34177  prter2  34660  ax4fromc4  34673  hbae-o  34682  dvelimf-o  34708  ax12indn  34722  ax12inda2  34726  ax12a2-o  34729  l1cvpat  34834  atcvrj0  35208  pmaple  35541  paddasslem5  35604  pclfinN  35680  osumcllem11N  35746  pexmidlem8N  35757  dvheveccl  36893  dihord6apre  37037  lpolconN  37268  isnacs3  37775  pellexlem5  37899  pellex  37901  jm2.18  38056  jm2.15nn0  38071  jm2.16nn0  38072  dford3lem2  38095  ttac  38104  acsfn1p  38270  rp-isfinite5  38363  cnvssb  38392  clcnvlem  38430  iunrelexpuztr  38511  rfovcnvf1od  38798  ntrrn  38920  nzss  39016  pm11.71  39097  axc11next  39106  hbntal  39267  eel2122old  39441  reuimrmo  41690  afvelima  41756  rlimdmafv  41766  rlimdmafv2  41847  sfprmdvdsmersenne  42095  perfectALTVlem2  42206  elsprel  42293  copisnmnd  42377  rnghmsscmap2  42541  rnghmsscmap  42542  rhmsscmap2  42587  rhmsscmap  42588  funcringcsetcALTV2lem8  42611  funcringcsetclem8ALTV  42634  lindslinindsimp2lem5  42819  nn0sumshdig  42985  spd  42993  setrec1lem4  43005  setrec2fun  43007  aacllem  43118
  Copyright terms: Public domain W3C validator