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  482  adantrd  483  impel  484  mpan9  485  pm4.79  606  pm2.36  906  pm4.72  938  ecased  1004  ecase3ad  1005  syl3an2  1400  syl2an23an  1427  19.38a  1807  19.38b  1808  alrimdh  1830  stdpc5v  1907  19.37imv  1915  ax12w  2050  ax13dgen2  2055  ax12v  2088  spsd  2095  nf5r  2102  axc4  2168  equs5eALT  2214  ax13lem1  2284  nfeqf  2337  hbae  2348  ax12vALT  2456  2ax6elem  2477  euimmo  2551  necon2ad  2838  necon4ad  2842  spcimgft  3315  rr19.28v  3378  moeq3  3416  sbeqalb  3521  csbexg  4825  reusv2lem2OLD  4900  ralxfrd  4909  ralxfrdOLD  4910  ralxfrd2  4914  ralxfrALT  4917  copsexg  4985  pwssun  5049  somo  5098  ssrel  5241  relssres  5472  issref  5544  dmsnopg  5642  dfco2a  5673  wfisg  5753  tz7.7  5787  ordunidif  5811  suctr  5846  trsucss  5849  suc11  5869  imadif  6011  fvelima  6287  dffv2  6310  fvmptd3f  6334  fvmptf  6340  fvmptnf  6341  foco2  6419  foco2OLD  6420  fconst5  6512  funfvima2  6533  funfvima3  6535  isores3  6625  riotaxfrd  6682  ovmpt4g  6825  ovmpt2s  6826  ov2gf  6827  ovmpt2df  6834  sorpsscmpl  6990  abnexg  7006  onint  7037  limuni3  7094  tfi  7095  tfis  7096  tfinds  7101  limomss  7112  peano5  7131  fo2ndf  7329  frxp  7332  suppssov1  7372  suppss2  7374  suppssfv  7376  rntpos  7410  tposf2  7421  wfr3g  7458  wfrlem4  7463  wfrlem5  7464  wfrlem17  7476  onfununi  7483  smofvon2  7498  smo11  7506  smoord  7507  tfrlem11  7529  tz7.44-2  7548  tz7.48lem  7581  tz7.48-1  7583  tz7.49  7585  tz7.49c  7586  omordi  7691  omord  7693  omass  7705  oneo  7706  omeulem1  7707  omopth2  7709  oewordri  7717  oeworde  7718  nnmordi  7756  nnmord  7757  omabs  7772  nnneo  7776  omsmo  7779  qsel  7869  eceqoveq  7895  mapsn  7941  f1oeng  8016  domunsncan  8101  sbthlem1  8111  2pwuninel  8156  mapen  8165  infensuc  8179  nneneq  8184  sucdom2  8197  pssnn  8219  dif1en  8234  findcard2  8241  ac6sfi  8245  frfi  8246  unblem1  8253  unblem2  8254  unbnn2  8258  nnsdomg  8260  xpfi  8272  domunfican  8274  fiint  8278  fodomfi  8280  ixpfi2  8305  finsschain  8314  marypha1lem  8380  oiexg  8481  brwdom3  8528  inf3lem2  8564  inf3lem3  8565  cantnfval2  8604  cantnflt  8607  cantnflem1  8624  cantnf  8628  cnfcom  8635  trcl  8642  epfrs  8645  r1sdom  8675  rankwflemb  8694  rankelb  8725  carden2a  8830  cardsdomel  8838  carduni  8845  harval2  8861  pr2ne  8866  infpwfien  8923  cardaleph  8950  carduniima  8957  alephval3  8971  dfac5  8989  dfac12r  9006  dfac12k  9007  kmlem11  9020  cdainf  9052  infxp  9075  cfsuc  9117  cfcoflem  9132  coftr  9133  cfcof  9134  infpssr  9168  fin23lem30  9202  isf32lem1  9213  isf34lem6  9240  fin1a2lem13  9272  fin1a2s  9274  axcc2lem  9296  domtriomlem  9302  axdc4lem  9315  axcclem  9317  ac6num  9339  zorn2lem5  9360  zorn2lem6  9361  axdclem2  9380  alephval2  9432  alephreg  9442  pwcfsdom  9443  axregndlem1  9462  axregnd  9464  axacndlem1  9467  axacndlem2  9468  axacndlem3  9469  axacndlem4  9470  axacnd  9472  gchi  9484  fpwwe2lem13  9502  canthp1  9514  gchpwdom  9530  wunfi  9581  tskwe2  9633  inar1  9635  gruen  9672  intgru  9674  indpi  9767  nqereu  9789  ltbtwnnq  9838  prnmadd  9857  genpcd  9866  prlem934  9893  ltexprlem1  9896  ltexprlem2  9897  ltexprlem7  9902  ltaprlem  9904  ltapr  9905  reclem4pr  9910  suplem2pr  9913  mulcmpblnr  9930  recexsrlem  9962  mulgt0sr  9964  recexsr  9966  supsrlem  9970  axpre-sup  10028  1re  10077  dedekindle  10239  addlsub  10485  recex  10697  nnunb  11326  0mnnnnn0  11363  prime  11496  zeo  11501  fnn0ind  11514  zindd  11516  btwnz  11517  lbzbi  11814  xrub  12180  elfznelfzo  12613  addmodlteq  12785  facwordi  13116  fiinfnf1o  13178  hashclb  13187  hashdom  13206  hashf1lem2  13278  seqcoll  13286  brfi1indALT  13320  ccatalpha  13411  swrdccatin12lem2a  13531  limsupbnd2  14258  rlimdm  14326  o1of2  14387  rlimno1  14428  isercoll  14442  climcau  14445  caurcvg2  14452  caucvgb  14454  serf0  14455  zsum  14493  fsum2dlem  14545  fsum2d  14546  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  zprod  14711  fprod2dlem  14754  fprod2d  14755  odd2np1  15112  ndvdssub  15180  dfgcd2  15310  coprmproddvdslem  15423  nprm  15448  maxprmfct  15468  rpexp  15479  pc2dvds  15630  pcfac  15650  unbenlem  15659  4sqlem12  15707  4sqlem17  15712  vdwlem6  15737  vdwlem13  15744  prmlem0  15859  xpscfv  16269  mreiincl  16303  sscfn1  16524  initoid  16702  termoid  16703  funcestrcsetclem8  16834  funcsetcestrclem8  16849  pospo  17020  cnvpsb  17260  dirref  17282  dirtr  17283  mulgaddcom  17611  mulginvcom  17612  gaass  17776  cntz2ss  17811  elsymgbas  17848  symgfix2  17882  pmtrfrn  17924  psgnran  17981  odmulg  18019  odhash3  18037  sylow2alem1  18078  sylow2alem2  18079  pj1eu  18155  efgs1b  18195  efgsfo  18198  efgredlemc  18204  efgredeu  18211  frgpuptinv  18230  lt6abl  18342  ghmcyg  18343  ablfac1eulem  18517  pgpfac1lem5  18524  ringinvnz1ne0  18638  irredn1  18752  irredmul  18755  lspextmo  19104  lspsncv0  19194  mplcoe1  19513  mplcoe5  19516  evlseu  19564  psgnghm  19974  mdetunilem7  20472  mdetunilem9  20474  chcoeffeq  20739  cnindis  21144  lmss  21150  lmcls  21154  lmcnp  21156  hausnei  21180  cmpsub  21251  tgcmp  21252  fiuncmp  21255  cmpfi  21259  bwth  21261  1stcrest  21304  2ndcdisj  21307  1stccnp  21313  comppfsc  21383  1stckgenlem  21404  txcls  21455  txcn  21477  txlm  21499  tx1stc  21501  xkococn  21511  hmphdis  21647  ptcmpfi  21664  isfild  21709  fgss2  21725  filconn  21734  trfil2  21738  ufileu  21770  filufint  21771  elfm2  21799  flftg  21847  fclssscls  21869  fclscf  21876  ufilcmp  21883  cnpfcf  21892  alexsubb  21897  alexsubALTlem4  21901  alexsubALT  21902  cnextcn  21918  qustgpopn  21970  tsmsxp  22005  isust  22054  xmettri2  22192  blin2  22281  setsmstopn  22330  met2ndc  22375  metcnp3  22392  tngtopn  22501  reconnlem2  22677  xrge0tsms  22684  fsumcn  22720  bndth  22804  iscmet3lem2  23136  iscmet3  23137  ivthlem1  23266  ivthlem2  23267  ivthlem3  23268  ovolfiniun  23315  volfiniun  23361  ioombl1lem4  23375  dyadmbl  23414  ismbf3d  23466  itg1addlem4  23511  mbfi1flimlem  23534  itg2seq  23554  itgfsum  23638  ellimc3  23688  dvmptfsum  23783  c1liplem1  23804  plypf1  24013  plydivex  24097  aannenlem1  24128  ulmval  24179  ulmcau  24194  ulmss  24196  ulmbdd  24197  ulmcn  24198  ulmdvlem3  24201  pserulm  24221  sineq0  24318  efopn  24449  cxpeq  24543  rlimcnp  24737  xrlimcnp  24740  perfectlem2  25000  lgsdir2lem2  25096  lgsne0  25105  2lgsoddprm  25186  2sqlem6  25193  2sqlem10  25198  dchrisumlem2  25224  axlowdimlem16  25882  axcontlem2  25890  uhgr0vb  26012  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  uvtxupgrres  26359  fusgrn0degnn0  26451  finsumvtxdg2size  26502  cusgrm1rusgr  26534  wlkv0  26603  uspgrn2crct  26756  frrusgrord  27321  numclwlk1lem2fo  27348  isgrpo  27479  grpoidinvlem3  27488  vcdi  27548  vcdir  27549  vcass  27550  nvs  27646  nvtri  27653  blocnilem  27787  chintcli  28318  hsupss  28328  shlej1  28347  elspansn4  28560  spansncvi  28639  hoaddsub  28803  lnopl  28901  lnfnl  28918  riesz4i  29050  pjnormssi  29155  pj3si  29194  stlei  29227  stcltr2i  29262  dmdmd  29287  dmdbr5  29295  mdslmd1lem2  29313  atssma  29365  atcvatlem  29372  chirredlem1  29377  atcvat4i  29384  mdsymlem2  29391  mdsymlem6  29395  sumdmdlem2  29406  cdjreui  29419  elimifd  29488  disjxpin  29527  unifi3  29618  xrge0infss  29653  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  xrge0tsmsd  29913  lmxrge0  30126  ismeas  30390  eulerpartlemb  30558  bnj849  31121  bnj1110  31176  connpconn  31343  cvmseu  31384  cvmliftlem15  31406  cvmlift2lem1  31410  cvmlift2lem12  31422  mclsind  31593  dfpo2  31771  fundmpss  31790  dfon2lem3  31814  dfon2lem4  31815  dfon2lem6  31817  dfon2lem8  31819  dfon2lem9  31820  hbntg  31835  tfisg  31840  dftrpred3g  31857  trpredrec  31862  frpoinsg  31866  frinsg  31870  soseq  31879  frr3g  31904  frrlem5  31909  sltval2  31934  noetalem3  31990  conway  32035  cgrdegen  32236  funtransport  32263  ifscgr  32276  cgrxfr  32287  brofs2  32309  brifs2  32310  idinside  32316  btwnconn1lem7  32325  btwnconn1lem11  32329  btwnconn1lem12  32330  btwnconn1lem14  32332  broutsideof2  32354  btwnoutside  32357  outsideoftr  32361  finminlem  32437  ntruni  32447  neibastop1  32479  ontgval  32555  ordtop  32560  ordcmp  32571  onint1  32573  bj-ax12w  32790  axc11n11r  32798  bj-ax12v3  32800  bj-hbaeb2  32930  bj-spcimdv  33009  bj-spcimdvv  33010  bj-sngltag  33096  bj-xtagex  33102  bj-0int  33180  bj-ismooredr  33189  bj-inftyexpiinj  33226  wl-ax13lem1  33417  wl-speqv  33438  wl-sbcom2d  33474  wl-ax11-lem3  33494  wl-ax11-lem8  33499  tan2h  33531  ptrest  33538  poimirlem20  33559  poimirlem22  33561  poimirlem26  33565  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  heicant  33574  voliunnfl  33583  volsupnfl  33584  itg2addnclem2  33592  itg2addnc  33594  itg2gt0cn  33595  ftc2nc  33624  filbcmb  33665  sdclem2  33668  seqpo  33673  nninfnub  33677  neificl  33679  prdstotbnd  33723  cnpwstotbnd  33726  heibor1lem  33738  heibor  33750  bfplem2  33752  opidonOLD  33781  exidu1  33785  grpokerinj  33822  rngoideu  33832  rngodi  33833  rngodir  33834  rngmgmbs4  33860  divrngidl  33957  prnc  33996  prter2  34485  ax4fromc4  34498  hbae-o  34507  dvelimf-o  34533  ax12indn  34547  ax12inda2  34551  ax12a2-o  34554  l1cvpat  34659  atcvrj0  35032  pmaple  35365  paddasslem5  35428  pclfinN  35504  osumcllem11N  35570  pexmidlem8N  35581  dvheveccl  36718  dihord6apre  36862  lpolconN  37093  isnacs3  37590  pellexlem5  37714  pellex  37716  jm2.18  37872  jm2.15nn0  37887  jm2.16nn0  37888  dford3lem2  37911  ttac  37920  acsfn1p  38086  rp-isfinite5  38180  cnvssb  38209  clcnvlem  38247  iunrelexpuztr  38328  rfovcnvf1od  38615  ntrrn  38737  nzss  38833  pm11.71  38914  axc11next  38924  hbntal  39086  eel2122old  39260  mapsnd  39702  reuimrmo  41499  afvelima  41568  rlimdmafv  41578  sfprmdvdsmersenne  41845  perfectALTVlem2  41956  elsprel  42050  copisnmnd  42134  rnghmsscmap2  42298  rnghmsscmap  42299  rhmsscmap2  42344  rhmsscmap  42345  funcringcsetcALTV2lem8  42368  funcringcsetclem8ALTV  42391  lindslinindsimp2lem5  42576  nn0sumshdig  42742  spd  42750  setrec1lem4  42762  setrec2fun  42764  aacllem  42875
  Copyright terms: Public domain W3C validator