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  483  adantrd  484  impel  485  mpan9  486  pm4.79  606  pm2.36  887  pm4.72  919  ecased  984  ecase3ad  985  syl3an2  1357  syl2an23an  1384  19.38a  1764  19.38b  1765  alrimdh  1787  stdpc5v  1864  ax12w  2007  ax13dgen2  2012  ax12v  2045  ax12vOLD  2047  ax12vOLDOLD  2048  spsd  2055  nf5r  2062  axc4  2126  equs5eALT  2177  ax13lem1  2247  nfeqf  2300  hbae  2314  ax12vALT  2427  2ax6elem  2448  euimmo  2521  necon2ad  2805  necon4ad  2809  spcimgft  3274  rr19.28v  3334  moeq3  3370  sbeqalb  3475  csbexg  4762  reusv2lem2OLD  4840  ralxfrd  4849  ralxfrdOLD  4850  ralxfrd2  4854  ralxfrALT  4857  copsexg  4926  pwssun  4990  somo  5039  ssrel  5178  relssres  5406  issref  5478  dmsnopg  5575  dfco2a  5604  wfisg  5684  tz7.7  5718  ordunidif  5742  suctr  5777  trsucss  5780  suc11  5800  imadif  5941  fvelima  6215  dffv2  6238  fvmptdf  6262  fvmptf  6267  fvmptnf  6268  foco2  6345  foco2OLD  6346  fconst5  6436  funfvima2  6458  funfvima3  6460  isores3  6550  riotaxfrd  6607  ovmpt4g  6748  ovmpt2s  6749  ov2gf  6750  ovmpt2df  6757  sorpsscmpl  6913  onint  6957  limuni3  7014  tfi  7015  tfis  7016  tfinds  7021  limomss  7032  peano5  7051  fo2ndf  7244  frxp  7247  suppssov1  7287  suppss2  7289  suppssfv  7291  rntpos  7325  tposf2  7336  wfr3g  7373  wfrlem4  7378  wfrlem5  7379  wfrlem17  7391  onfununi  7398  smofvon2  7413  smo11  7421  smoord  7422  tfrlem11  7444  tz7.44-2  7463  tz7.48lem  7496  tz7.48-1  7498  tz7.49  7500  tz7.49c  7501  omordi  7606  omord  7608  omass  7620  oneo  7621  omeulem1  7622  omopth2  7624  oewordri  7632  oeworde  7633  nnmordi  7671  nnmord  7672  omabs  7687  nnneo  7691  omsmo  7694  qsel  7786  eceqoveq  7813  mapsn  7859  f1oeng  7934  domunsncan  8020  sbthlem1  8030  2pwuninel  8075  mapen  8084  infensuc  8098  nneneq  8103  sucdom2  8116  pssnn  8138  dif1en  8153  findcard2  8160  ac6sfi  8164  frfi  8165  unblem1  8172  unblem2  8173  unbnn2  8177  nnsdomg  8179  xpfi  8191  domunfican  8193  fiint  8197  fodomfi  8199  ixpfi2  8224  finsschain  8233  marypha1lem  8299  oiexg  8400  brwdom3  8447  inf3lem2  8486  inf3lem3  8487  cantnfval2  8526  cantnflt  8529  cantnflem1  8546  cantnf  8550  cnfcom  8557  trcl  8564  epfrs  8567  r1sdom  8597  rankwflemb  8616  rankelb  8647  carden2a  8752  cardsdomel  8760  carduni  8767  harval2  8783  pr2ne  8788  infpwfien  8845  cardaleph  8872  carduniima  8879  alephval3  8893  dfac5  8911  dfac12r  8928  dfac12k  8929  kmlem11  8942  cdainf  8974  infxp  8997  cfsuc  9039  cfcoflem  9054  coftr  9055  cfcof  9056  infpssr  9090  fin23lem30  9124  isf32lem1  9135  isf34lem6  9162  fin1a2lem13  9194  fin1a2s  9196  axcc2lem  9218  domtriomlem  9224  axdc4lem  9237  axcclem  9239  ac6num  9261  zorn2lem5  9282  zorn2lem6  9283  axdclem2  9302  alephval2  9354  alephreg  9364  pwcfsdom  9365  axregndlem1  9384  axregnd  9386  axacndlem1  9389  axacndlem2  9390  axacndlem3  9391  axacndlem4  9392  axacnd  9394  gchi  9406  fpwwe2lem13  9424  canthp1  9436  gchpwdom  9452  wunfi  9503  tskwe2  9555  inar1  9557  gruen  9594  intgru  9596  indpi  9689  nqereu  9711  ltbtwnnq  9760  prnmadd  9779  genpcd  9788  prlem934  9815  ltexprlem1  9818  ltexprlem2  9819  ltexprlem7  9824  ltaprlem  9826  ltapr  9827  reclem4pr  9832  suplem2pr  9835  mulcmpblnr  9852  recexsrlem  9884  mulgt0sr  9886  recexsr  9888  supsrlem  9892  axpre-sup  9950  1re  9999  dedekindle  10161  addlsub  10407  recex  10619  nnunb  11248  0mnnnnn0  11285  prime  11418  zeo  11423  fnn0ind  11436  zindd  11438  btwnz  11439  lbzbi  11736  xrub  12101  elfznelfzo  12530  addmodlteq  12701  facwordi  13032  fiinfnf1o  13094  hashclb  13105  hashdom  13124  hashf1lem2  13194  seqcoll  13202  brfi1indALT  13237  brfi1indALTOLD  13243  ccatalpha  13330  swrdccatin12lem2a  13438  limsupbnd2  14164  rlimdm  14232  o1of2  14293  rlimno1  14334  isercoll  14348  climcau  14351  caurcvg2  14358  caucvgb  14360  serf0  14361  zsum  14398  fsum2dlem  14448  fsum2d  14449  fsumabs  14479  fsumrlim  14489  fsumo1  14490  fsumiun  14499  zprod  14611  fprod2dlem  14654  fprod2d  14655  odd2np1  15008  ndvdssub  15076  dfgcd2  15206  coprmproddvdslem  15319  nprm  15344  maxprmfct  15364  rpexp  15375  pc2dvds  15526  pcfac  15546  unbenlem  15555  4sqlem12  15603  4sqlem17  15608  vdwlem6  15633  vdwlem13  15640  prmlem0  15755  xpscfv  16162  mreiincl  16196  sscfn1  16417  initoid  16595  termoid  16596  funcestrcsetclem8  16727  funcsetcestrclem8  16742  pospo  16913  cnvpsb  17153  dirref  17175  dirtr  17176  mulgaddcom  17504  mulginvcom  17505  gaass  17670  cntz2ss  17705  elsymgbas  17742  symgfix2  17776  pmtrfrn  17818  psgnran  17875  odmulg  17913  odhash3  17931  sylow2alem1  17972  sylow2alem2  17973  pj1eu  18049  efgs1b  18089  efgsfo  18092  efgredlemc  18098  efgredeu  18105  frgpuptinv  18124  lt6abl  18236  ghmcyg  18237  ablfac1eulem  18411  pgpfac1lem5  18418  ringinvnz1ne0  18532  irredn1  18646  irredmul  18649  lspextmo  18996  lspsncv0  19086  mplcoe1  19405  mplcoe5  19408  evlseu  19456  psgnghm  19866  mdetunilem7  20364  mdetunilem9  20366  chcoeffeq  20631  cnindis  21036  lmss  21042  lmcls  21046  lmcnp  21048  hausnei  21072  cmpsub  21143  tgcmp  21144  fiuncmp  21147  cmpfi  21151  bwth  21153  1stcrest  21196  2ndcdisj  21199  1stccnp  21205  comppfsc  21275  1stckgenlem  21296  txcls  21347  txcn  21369  txlm  21391  tx1stc  21393  xkococn  21403  hmphdis  21539  ptcmpfi  21556  isfild  21602  fgss2  21618  filconn  21627  trfil2  21631  ufileu  21663  filufint  21664  elfm2  21692  flftg  21740  fclssscls  21762  fclscf  21769  ufilcmp  21776  cnpfcf  21785  alexsubb  21790  alexsubALTlem4  21794  alexsubALT  21795  cnextcn  21811  qustgpopn  21863  tsmsxp  21898  isust  21947  xmettri2  22085  blin2  22174  setsmstopn  22223  met2ndc  22268  metcnp3  22285  tngtopn  22394  reconnlem2  22570  xrge0tsms  22577  fsumcn  22613  bndth  22697  iscmet3lem2  23030  iscmet3  23031  ivthlem1  23160  ivthlem2  23161  ivthlem3  23162  ovolfiniun  23209  volfiniun  23255  ioombl1lem4  23269  dyadmbl  23308  ismbf3d  23361  itg1addlem4  23406  mbfi1flimlem  23429  itg2seq  23449  itgfsum  23533  ellimc3  23583  dvmptfsum  23676  c1liplem1  23697  plypf1  23906  plydivex  23990  aannenlem1  24021  ulmval  24072  ulmcau  24087  ulmss  24089  ulmbdd  24090  ulmcn  24091  ulmdvlem3  24094  pserulm  24114  sineq0  24211  efopn  24338  cxpeq  24432  rlimcnp  24626  xrlimcnp  24629  perfectlem2  24889  lgsdir2lem2  24985  lgsne0  24994  2lgsoddprm  25075  2sqlem6  25082  2sqlem10  25087  dchrisumlem2  25113  axlowdimlem16  25771  axcontlem2  25779  uhgr0vb  25897  uvtxa01vtx0  26218  uvtxupgrres  26230  fusgrn0degnn0  26315  cusgrm1rusgr  26382  wlkv0  26450  uspgrn2crct  26603  isgrpo  27239  grpoidinvlem3  27248  vcdi  27308  vcdir  27309  vcass  27310  nvs  27406  nvtri  27413  blocnilem  27547  chintcli  28078  hsupss  28088  shlej1  28107  elspansn4  28320  spansncvi  28399  hoaddsub  28563  lnopl  28661  lnfnl  28678  riesz4i  28810  pjnormssi  28915  pj3si  28954  stlei  28987  stcltr2i  29022  dmdmd  29047  dmdbr5  29055  mdslmd1lem2  29073  atssma  29125  atcvatlem  29132  chirredlem1  29137  atcvat4i  29144  mdsymlem2  29151  mdsymlem6  29155  sumdmdlem2  29166  cdjreui  29179  elimifd  29250  disjxpin  29287  unifi3  29374  xrge0infss  29410  gsumle  29606  gsumvsca1  29609  gsumvsca2  29610  xrge0tsmsd  29612  lmxrge0  29822  ismeas  30085  eulerpartlemb  30253  bnj849  30756  bnj1110  30811  connpconn  30978  cvmseu  31019  cvmliftlem15  31041  cvmlift2lem1  31045  cvmlift2lem12  31057  mclsind  31228  dfpo2  31406  fundmpss  31421  dfon2lem3  31444  dfon2lem4  31445  dfon2lem6  31447  dfon2lem8  31449  dfon2lem9  31450  hbntg  31465  tfisg  31470  dftrpred3g  31487  trpredrec  31492  frinsg  31496  soseq  31505  frr3g  31533  frrlem4  31537  frrlem5  31538  sltval2  31563  nodenselem5  31601  cgrdegen  31806  funtransport  31833  ifscgr  31846  cgrxfr  31857  brofs2  31879  brifs2  31880  idinside  31886  btwnconn1lem7  31895  btwnconn1lem11  31899  btwnconn1lem12  31900  btwnconn1lem14  31902  broutsideof2  31924  btwnoutside  31927  outsideoftr  31931  finminlem  32007  ntruni  32017  neibastop1  32049  ontgval  32125  ordtop  32130  ordcmp  32141  onint1  32143  bj-ax12w  32360  axc11n11r  32368  bj-ax12v3  32370  bj-hbaeb2  32501  bj-spcimdv  32584  bj-spcimdvv  32585  bj-sngltag  32671  bj-xtagex  32677  bj-inftyexpiinj  32768  wl-ax13lem1  32958  wl-speqv  32979  wl-sbcom2d  33015  wl-ax11-lem3  33035  wl-ax11-lem8  33040  tan2h  33072  ptrest  33079  poimirlem20  33100  poimirlem22  33102  poimirlem26  33106  poimirlem30  33110  poimirlem31  33111  poimirlem32  33112  heicant  33115  voliunnfl  33124  volsupnfl  33125  itg2addnclem2  33133  itg2addnc  33135  itg2gt0cn  33136  ftc2nc  33165  filbcmb  33206  sdclem2  33209  seqpo  33214  nninfnub  33218  neificl  33220  prdstotbnd  33264  cnpwstotbnd  33267  heibor1lem  33279  heibor  33291  bfplem2  33293  opidonOLD  33322  exidu1  33326  grpokerinj  33363  rngoideu  33373  rngodi  33374  rngodir  33375  rngmgmbs4  33401  divrngidl  33498  prnc  33537  prter2  33685  ax4fromc4  33698  hbae-o  33707  dvelimf-o  33733  ax12indn  33747  ax12inda2  33751  ax12a2-o  33754  l1cvpat  33860  atcvrj0  34233  pmaple  34566  paddasslem5  34629  pclfinN  34705  osumcllem11N  34771  pexmidlem8N  34782  dvheveccl  35920  dihord6apre  36064  lpolconN  36295  isnacs3  36792  pellexlem5  36916  pellex  36918  jm2.18  37074  jm2.15nn0  37089  jm2.16nn0  37090  dford3lem2  37113  ttac  37122  acsfn1p  37289  rp-isfinite5  37383  cnvssb  37412  clcnvlem  37450  iunrelexpuztr  37531  rfovcnvf1od  37819  ntrrn  37941  nzss  38037  pm11.71  38118  axc11next  38128  hbntal  38290  eel2122old  38464  mapsnd  38897  reuimrmo  40512  afvelima  40581  rlimdmafv  40591  sfprmdvdsmersenne  40849  perfectALTVlem2  40956  elsprel  41043  copisnmnd  41127  rnghmsscmap2  41291  rnghmsscmap  41292  rhmsscmap2  41337  rhmsscmap  41338  funcringcsetcALTV2lem8  41361  funcringcsetclem8ALTV  41384  lindslinindsimp2lem5  41569  nn0sumshdig  41739  spd  41747  setrec1lem4  41760  setrec2fun  41762  aacllem  41880
  Copyright terms: Public domain W3C validator