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

Theorem syl5 33
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  35  syl2im  39  imim12i  59  peirceroll  82  pm2.86d  104  con2d  127  con3d  146  nsyli  153  syl5bi  230  syl5bir  231  syl5ib  232  adantld  481  adantrd  482  impel  483  mpan9  484  pm4.79  604  pm2.36  883  pm4.72  915  ecased  981  ecase3ad  982  syl3an2  1351  syl2an23an  1378  alrimdh  1776  stdpc5v  1853  ax12w  1996  ax13dgen2  2001  ax12v  2034  ax12vOLD  2036  ax12vOLDOLD  2037  spsd  2044  nf5r  2051  axc4  2114  equs5eALT  2165  ax13lem1  2235  nfeqf  2288  hbae  2302  ax12vALT  2415  2ax6elem  2436  euimmo  2509  necon2ad  2796  necon4ad  2800  spcimgft  3256  rr19.28v  3314  moeq3  3349  sbeqalb  3454  triun  4688  csbexg  4714  reusv2lem2OLD  4790  ralxfrd  4799  ralxfrdOLD  4800  ralxfrd2  4804  ralxfrALT  4807  copsexg  4875  pwssun  4933  somo  4982  relssres  5343  issref  5414  dmsnopg  5509  dfco2a  5537  wfisg  5617  tz7.7  5651  ordunidif  5675  suctr  5710  trsucss  5713  suc11  5733  imadif  5872  fvelima  6142  dffv2  6165  fvmptdf  6188  fvmptf  6193  fvmptnf  6194  foco2  6271  foco2OLD  6272  fconst5  6353  funfvima2  6374  funfvima3  6376  isores3  6462  riotaxfrd  6518  oprabid  6553  ovmpt4g  6658  ovmpt2s  6659  ov2gf  6660  ovmpt2df  6667  sorpsscmpl  6823  onint  6864  limuni3  6921  tfi  6922  tfis  6923  tfinds  6928  limomss  6939  peano5  6958  fo2ndf  7148  frxp  7151  suppssov1  7191  suppss2  7193  suppssfv  7195  rntpos  7229  tposf2  7240  wfr3g  7277  wfrlem4  7282  wfrlem5  7283  wfrlem17  7295  onfununi  7302  smofvon2  7317  smo11  7325  smoord  7326  tfrlem11  7348  tz7.44-2  7367  tz7.48lem  7400  tz7.48-1  7402  tz7.49  7404  tz7.49c  7405  omordi  7510  omord  7512  omass  7524  oneo  7525  omeulem1  7526  omopth2  7528  oewordri  7536  oeworde  7537  nnmordi  7575  nnmord  7576  omabs  7591  nnneo  7595  omsmo  7598  ectocld  7678  qsel  7690  eceqoveq  7717  mapsn  7762  f1oeng  7837  domunsncan  7922  sbthlem1  7932  2pwuninel  7977  mapen  7986  infensuc  8000  nneneq  8005  sucdom2  8018  pssnn  8040  dif1en  8055  findcard2  8062  ac6sfi  8066  frfi  8067  unblem1  8074  unblem2  8075  unbnn2  8079  nnsdomg  8081  xpfi  8093  domunfican  8095  fiint  8099  fodomfi  8101  ixpfi2  8124  finsschain  8133  marypha1lem  8199  oiexg  8300  brwdom3  8347  inf3lem2  8386  inf3lem3  8387  cantnfval2  8426  cantnflt  8429  cantnflem1  8446  cantnf  8450  cnfcom  8457  trcl  8464  epfrs  8467  r1sdom  8497  rankwflemb  8516  rankpwi  8546  rankelb  8547  carden2a  8652  cardsdomel  8660  carduni  8667  harval2  8683  pr2ne  8688  infpwfien  8745  cardaleph  8772  carduniima  8779  alephval3  8793  dfac5  8811  dfac12r  8828  dfac12k  8829  kmlem4  8835  kmlem11  8842  kmlem12  8843  cdainf  8874  infxp  8897  cfsuc  8939  cfcoflem  8954  coftr  8955  cfcof  8956  infpssr  8990  fin23lem30  9024  isf32lem1  9035  isf34lem6  9062  fin1a2lem13  9094  fin1a2s  9096  axcc2lem  9118  domtriomlem  9124  axdc4lem  9137  axcclem  9139  ac6num  9161  zorn2lem5  9182  zorn2lem6  9183  axdclem2  9202  alephval2  9250  alephreg  9260  pwcfsdom  9261  axregndlem1  9280  axregnd  9282  axacndlem1  9285  axacndlem2  9286  axacndlem3  9287  axacndlem4  9288  axacnd  9290  gchi  9302  fpwwe2lem13  9320  canthp1  9332  gchpwdom  9348  wunfi  9399  tskwe2  9451  inar1  9453  gruen  9490  intgru  9492  indpi  9585  nqereu  9607  ltbtwnnq  9656  prnmadd  9675  genpcd  9684  prlem934  9711  ltexprlem1  9714  ltexprlem2  9715  ltexprlem7  9720  ltaprlem  9722  ltapr  9723  reclem4pr  9728  suplem2pr  9731  mulcmpblnr  9748  recexsrlem  9780  mulgt0sr  9782  recexsr  9784  supsrlem  9788  axpre-sup  9846  1re  9895  dedekindle  10052  addlsub  10298  recex  10510  nnunb  11137  0mnnnnn0  11174  prime  11292  zeo  11297  fnn0ind  11310  zindd  11312  btwnz  11313  lbzbi  11610  xrub  11972  elfznelfzo  12396  addmodlteq  12564  facwordi  12895  fiinfnf1o  12954  hashclb  12965  hashdom  12983  hashf1lem2  13051  seqcoll  13059  hash2pwpr  13067  brfi1indALT  13085  brfi1indALTOLD  13091  ccatalpha  13176  swrdccatin12lem2a  13284  limsupbnd2  14010  rlimdm  14078  o1of2  14139  rlimno1  14180  isercoll  14194  climcau  14197  caurcvg2  14204  caucvgb  14206  serf0  14207  zsum  14244  fsum2dlem  14291  fsum2d  14292  fsumabs  14322  fsumrlim  14332  fsumo1  14333  fsumiun  14342  incexclem  14355  zprod  14454  fprod2dlem  14497  fprod2d  14498  odd2np1  14851  ndvdssub  14919  dfgcd2  15049  coprmproddvdslem  15162  nprm  15187  maxprmfct  15207  rpexp  15218  pc2dvds  15369  pcfac  15389  unbenlem  15398  4sqlem12  15446  4sqlem17  15451  vdwlem6  15476  vdwlem13  15483  prmlem0  15598  xpscfv  15993  mreiincl  16027  sscfn1  16248  initoid  16426  termoid  16427  funcestrcsetclem8  16558  funcsetcestrclem8  16573  pospo  16744  cnvpsb  16984  dirref  17006  dirtr  17007  mulgaddcom  17335  mulginvcom  17336  gaass  17501  cntz2ss  17536  elsymgbas  17573  symgfix2  17607  pmtrfrn  17649  psgnran  17706  odmulg  17744  odhash3  17762  sylow2alem1  17803  sylow2alem2  17804  pj1eu  17880  efgs1b  17920  efgsfo  17923  efgredlemc  17929  efgredeu  17936  frgpuptinv  17955  lt6abl  18067  ghmcyg  18068  ablfac1eulem  18242  pgpfac1lem5  18249  ringinvnz1ne0  18363  irredn1  18477  irredmul  18480  lspextmo  18825  lspsncv0  18915  mplcoe1  19234  mplcoe5  19237  evlseu  19285  cygth  19686  psgnghm  19692  mdetunilem7  20190  mdetunilem9  20192  chcoeffeq  20457  cnpco  20828  cnindis  20853  lmss  20859  lmcls  20863  lmcnp  20865  hausnei  20889  cmpsub  20960  tgcmp  20961  fiuncmp  20964  cmpfi  20968  bwth  20970  1stcrest  21013  2ndcdisj  21016  1stccnp  21022  comppfsc  21092  1stckgenlem  21113  txcls  21164  txcn  21186  txlm  21208  tx1stc  21210  txkgen  21212  xkococn  21220  hmphdis  21356  ptcmpfi  21373  isfild  21419  fgss2  21435  filcon  21444  trfil2  21448  ufileu  21480  filufint  21481  elfm2  21509  flftg  21557  cnpflf2  21561  fclssscls  21579  fclscf  21586  ufilcmp  21593  cnpfcf  21602  alexsubb  21607  alexsubALTlem4  21611  alexsubALT  21612  cnextcn  21628  qustgpopn  21680  tsmsxp  21715  isust  21764  xmettri2  21902  blin2  21991  setsmstopn  22040  met2ndc  22085  metcnp3  22102  tngtopn  22211  reconnlem2  22385  xrge0tsms  22392  fsumcn  22428  bndth  22512  iscmet3lem2  22842  iscmet3  22843  ivthlem1  22971  ivthlem2  22972  ivthlem3  22973  ovolfiniun  23020  volfiniun  23066  ioombl1lem4  23080  dyadmbl  23118  ismbf3d  23171  itg1addlem4  23216  mbfi1flimlem  23239  itg2seq  23259  itgfsum  23343  ellimc3  23393  dvmptfsum  23486  c1liplem1  23507  plypf1  23716  plydivex  23800  aannenlem1  23831  ulmval  23882  ulmcau  23897  ulmss  23899  ulmbdd  23900  ulmcn  23901  ulmdvlem3  23904  pserulm  23924  sineq0  24021  efopn  24148  cxpeq  24242  rlimcnp  24436  xrlimcnp  24439  perfectlem2  24699  lgsdir2lem2  24795  lgsne0  24804  2lgsoddprm  24885  2sqlem6  24892  2sqlem10  24897  dchrisumlem2  24923  axlowdimlem16  25582  axcontlem2  25590  usgrcyclnl1  25961  4cycl4dv  25988  el2wlkonot  26189  2wlkonot3v  26195  2spthonot3v  26196  cusgraiffrusgra  26260  2pthfrgra  26331  isgrpo  26528  grpoidinvlem3  26537  vcdi  26597  vcdir  26598  vcass  26599  nvs  26695  nvtri  26702  blocnilem  26836  chintcli  27367  hsupss  27377  shlej1  27396  elspansn4  27609  spansncvi  27688  hoaddsub  27852  lnopl  27950  lnfnl  27967  riesz4i  28099  pjnormssi  28204  pj3si  28243  stlei  28276  stcltr2i  28311  dmdmd  28336  dmdbr5  28344  mdslmd1lem2  28362  atssma  28414  atcvatlem  28421  chirredlem1  28426  atcvat4i  28433  mdsymlem2  28440  mdsymlem6  28444  sumdmdlem2  28455  dmdbr5ati  28458  cdjreui  28468  elimifd  28539  disjxpin  28576  unifi3  28666  xrge0infss  28708  gsumle  28903  gsumvsca1  28906  gsumvsca2  28907  xrge0tsmsd  28909  lmxrge0  29119  ismeas  29382  eulerpartlemb  29550  bnj849  30042  bnj1110  30097  conpcon  30264  cvmseu  30305  cvmliftlem15  30327  cvmlift2lem1  30331  cvmlift2lem12  30343  mclsind  30514  dfpo2  30691  fundmpss  30703  dfon2lem3  30727  dfon2lem4  30728  dfon2lem6  30730  dfon2lem8  30732  dfon2lem9  30733  hbntg  30748  tfisg  30753  dftrpred3g  30770  trpredrec  30775  frinsg  30779  soseq  30788  frr3g  30816  frrlem4  30820  frrlem5  30821  sltval2  30846  nodenselem5  30877  cgrdegen  31074  funtransport  31101  ifscgr  31114  cgrxfr  31125  brofs2  31147  brifs2  31148  idinside  31154  btwnconn1lem7  31163  btwnconn1lem11  31167  btwnconn1lem12  31168  btwnconn1lem14  31170  broutsideof2  31192  btwnoutside  31195  outsideoftr  31199  finminlem  31275  ntruni  31285  neibastop1  31317  ontgval  31393  ordtop  31398  ordcmp  31409  onint1  31411  bj-ax12w  31645  axc11n11r  31653  bj-ax12v3  31655  bj-hbaeb2  31786  bj-spcimdv  31861  bj-sngltag  31947  bj-xtagex  31953  bj-inftyexpiinj  32056  wl-ax13lem1  32249  wl-speqv  32270  wl-sbcom2d  32306  wl-ax11-lem3  32326  wl-ax11-lem8  32331  tan2h  32354  ptrest  32361  ptrecube  32362  poimirlem20  32382  poimirlem22  32384  poimirlem26  32388  poimirlem30  32392  poimirlem31  32393  poimirlem32  32394  heicant  32397  voliunnfl  32406  volsupnfl  32407  itg2addnclem2  32415  itg2addnc  32417  itg2gt0cn  32418  ftc2nc  32447  filbcmb  32488  sdclem2  32491  seqpo  32496  nninfnub  32500  neificl  32502  prdstotbnd  32546  cnpwstotbnd  32549  heibor1lem  32561  heibor  32573  bfplem2  32575  opidonOLD  32604  exidu1  32608  grpokerinj  32645  rngoideu  32655  rngodi  32656  rngodir  32657  rngmgmbs4  32683  divrngidl  32780  prnc  32819  prter2  32967  ax4fromc4  32980  hbae-o  32989  dvelimf-o  33015  ax12indn  33029  ax12inda2  33033  ax12a2-o  33036  l1cvpat  33142  atcvrj0  33515  pmaple  33848  paddasslem5  33911  pclfinN  33987  osumcllem11N  34053  pexmidlem8N  34064  dvheveccl  35202  dihord6apre  35346  lpolconN  35577  isnacs3  36074  pellexlem5  36198  pellex  36200  jm2.18  36356  jm2.15nn0  36371  jm2.16nn0  36372  dford3lem2  36395  ttac  36404  acsfn1p  36571  rp-isfinite5  36665  cnvssb  36694  clcnvlem  36732  iunrelexpuztr  36813  rfovcnvf1od  37101  ntrrn  37223  nzss  37321  pm11.71  37402  axc11next  37412  hbntal  37573  eel2122old  37747  mapsnd  38166  reuimrmo  39610  afvelima  39680  rlimdmafv  39690  sfprmdvdsmersenne  39842  perfectALTVlem2  39949  uhgr0vb  40278  uvtxa01vtx0  40604  uvtxupgrres  40616  fusgrn0degnn0  40695  cusgrm1rusgr  40763  1wlkv0  40840  uspgrn2crct  40992  copisnmnd  41580  rnghmsscmap2  41746  rnghmsscmap  41747  rhmsscmap2  41792  rhmsscmap  41793  funcringcsetcALTV2lem8  41816  funcringcsetclem8ALTV  41839  lindslinindsimp2lem5  42026  nn0sumshdig  42196  aacllem  42298
  Copyright terms: Public domain W3C validator