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

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5com 31	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  pm2.86d  108  con2d  134  con3d  152  nsyli  157  biimtrid  244  biimtrrid  245  imbitrid  246  adantld  494  adantrd  495  impel  513  mpan9  514  pm4.72  962  pm2.36  982  pm4.79  1016  ecased  1046  alrimdh  1882  stdpc5v  1957  19.37imv  1966  ax12w  2166  ax13dgen2  2171  ax12v  2212  spsd  2221  nf5r  2228  axc4  2352  equs5eALT  2397  ax13lem1  2404  nfeqf  2411  hbae  2461  ax12vALT  2499  2ax6elem  2500  sb1  2508  euimmo  2642  necon2ad  2971  necon4ad  2975  r19.37v  3187  spcimgfi1OLD  3515  rr19.28v  3627  moeq3  3674  reuimrmo  3707  sbeqalb  3806  replem  5237  csbexg  5259  ralxfrd  5364  ralxfrd2  5368  ralxfrALT  5371  copsexgwOLD  5458  copsexg  5459  pwssun  5537  somo  5592  ssrel  5753  relssres  6006  dmsnopg  6196  dfco2a  6229  dfpo2  6279  frpoinsg  6326  tz7.7  6368  ordunidif  6392  suctr  6430  trsucss  6432  suc11  6451  imadif  6601  dffv2  6958  fvmptd3f  6987  fvmptnf  6994  foco2  7086  fconst5  7186  fvf1pr  7287  isores3  7315  riotaxfrd  7383  ovmpt4g  7539  ovmpos  7540  ov2gf  7541  ovmpodf  7548  sorpsscmpl  7713  abnexg  7735  onint  7769  limuni3  7828  tfisg  7830  tfis  7831  tfinds  7836  limomss  7847  peano5  7870  fo2ndf  8095  frxp  8101  xpord2pred  8120  xpord2indlem  8122  soseq  8134  suppss2  8175  suppssfv  8177  rntpos  8214  fprlem1  8276  fprresex  8286  wfr3g  8295  onfununi  8307  smofvon2  8322  smo11  8330  smoord  8331  tfrlem11  8354  tz7.44-2  8373  tz7.48lem  8407  tz7.48-1  8409  tz7.49  8411  tz7.49c  8412  omordi  8530  omord  8532  omass  8544  oneo  8545  omeulem1  8546  omopth2  8548  oewordri  8557  oeworde  8558  nnmordi  8596  nnmord  8597  omabs  8616  nnneo  8620  omsmo  8623  naddcllem  8641  qsel  8773  eceqoveq  8799  domunsncan  9045  sbthlem1  9055  2pwuninel  9100  mapen  9109  infensuc  9123  rexdif1en  9125  findcard2  9129  pssnn  9133  ssfi  9137  sucdom2  9167  php  9171  onomeneq  9178  0sdom1dom  9186  sdom1  9190  dif1ennnALT  9217  ac6sfi  9224  frfi  9225  unblem1  9232  unblem2  9233  unbnn2  9237  domunfican  9262  fodomfir  9268  ixpfi2  9290  finsschain  9299  unifi3  9302  marypha1lem  9376  oiexg  9480  brwdom3  9527  inf3lem2  9581  inf3lem3  9582  cantnfval2  9621  cantnflt  9624  cantnflem1  9641  cnfcom  9652  ttrclss  9672  trcl  9680  epfrs  9683  frmin  9704  frinsg  9706  frr3g  9711  frrlem15  9712  r1sdom  9729  cardsdomel  9929  carduni  9936  infpwfien  10015  carduniima  10049  dfac5  10082  dfac12r  10100  dfac12k  10101  kmlem11  10114  djuinf  10142  infxp  10167  cfsuc  10211  cfcoflem  10226  coftr  10227  infpssr  10262  fin23lem30  10296  isf32lem1  10307  isf34lem6  10334  fin1a2lem13  10366  fin1a2s  10368  axcc2lem  10390  domtriomlem  10396  axcclem  10411  ac6num  10433  zorn2lem5  10454  zorn2lem6  10455  axdclem2  10474  alephval2  10527  alephreg  10537  pwcfsdom  10538  axregndlem1  10557  axregnd  10559  axacndlem1  10562  axacndlem2  10563  axacndlem3  10564  axacndlem4  10565  axacnd  10567  gchi  10579  fpwwe2lem12  10597  canthp1  10609  gchpwdom  10625  wunfi  10676  tskwe2  10728  inar1  10730  gruen  10767  intgru  10769  indpi  10862  nqereu  10884  ltbtwnnq  10933  prnmadd  10952  genpcd  10961  prlem934  10988  ltexprlem1  10991  ltexprlem2  10992  ltexprlem7  10997  ltaprlem  10999  ltapr  11000  reclem4pr  11005  suplem2pr  11008  mulcmpblnr  11026  recexsrlem  11058  mulgt0sr  11060  supsrlem  11066  axpre-sup  11124  1re  11178  dedekindle  11344  addlsub  11600  recex  11816  nnunb  12474  0mnnnnn0  12510  prime  12651  zeo  12656  fnn0ind  12669  zindd  12671  btwnz  12673  lbzbi  12934  xrub  13312  elfznelfzo  13776  fvf1tp  13796  addmodlteq  13956  facwordi  14299  fiinfnf1o  14360  hashclb  14368  hashdom  14389  hashf1lem2  14466  seqcoll  14474  brfi1indALT  14520  ccatalpha  14604  pfxccatin12lem2a  14737  limsupbnd2  15493  rlimdm  15561  o1of2  15623  rlimno1  15664  isercoll  15678  caurcvg2  15688  caucvgb  15690  serf0  15691  zsum  15728  fsum2dlem  15780  fsum2d  15781  fsumabs  15812  fsumrlim  15822  fsumo1  15823  fsumiun  15832  zprod  15950  fprod2dlem  15993  fprod2d  15994  odd2np1  16358  ndvdssub  16426  dfgcd2  16563  nprm  16705  maxprmfct  16727  rpexp  16740  pc2dvds  16898  pcfac  16918  unbenlem  16927  4sqlem12  16975  4sqlem17  16980  vdwlem13  17012  prmlem0  17124  mreiincl  17607  sscfn1  17833  initoid  18017  termoid  18018  funcestrcsetclem8  18162  funcsetcestrclem8  18177  pospo  18358  cnvpsb  18594  dirtr  18617  mulgaddcom  19123  mulginvcom  19124  gaass  19320  cntz2ss  19358  elsymgbas  19397  symgfix2  19439  pmtrfrn  19481  psgnran  19538  odmulg  19579  odhash3  19599  sylow2alem1  19640  sylow2alem2  19641  pj1eu  19719  efgs1b  19759  efgsfo  19762  efgredlemc  19768  efgredeu  19775  frgpuptinv  19794  lt6abl  19918  ghmcyg  19919  ablfac1eulem  20097  pgpfac1lem5  20104  ablsimpgfindlem1  20132  gsumle  20168  ringinvnz1ne0  20329  irredmul  20457  rnghmsscmap2  20658  rnghmsscmap  20659  rhmsscmap2  20687  rhmsscmap  20688  acsfn1p  20828  lspextmo  21103  lspsncv0  21196  pzriprnglem12  21524  psgnghm  21612  mplcoe1  22070  mplcoe5  22073  evlseu  22116  mhpsclcl  22192  mdetunilem7  22658  mdetunilem9  22660  chcoeffeq  22926  cnindis  23332  lmss  23338  lmcls  23342  lmcnp  23344  hausnei  23368  cmpsub  23440  tgcmp  23441  fiuncmp  23444  cmpfi  23448  bwth  23450  1stcrest  23493  2ndcdisj  23496  1stccnp  23502  comppfsc  23572  1stckgenlem  23593  txcls  23644  txcn  23666  txlm  23688  tx1stc  23690  xkococn  23700  hmphdis  23836  ptcmpfi  23853  isfild  23898  fgss2  23914  filconn  23923  trfil2  23927  ufileu  23959  filufint  23960  elfm2  23988  flftg  24036  fclssscls  24058  fclscf  24065  ufilcmp  24072  cnpfcf  24081  alexsubb  24086  alexsubALTlem4  24090  alexsubALT  24091  qustgpopn  24160  tsmsxp  24195  isust  24244  xmettri2  24380  blin2  24469  setsmstopn  24518  met2ndc  24563  metcnp3  24580  tngtopn  24690  reconnlem2  24868  xrge0tsms  24875  fsumcn  24912  bndth  25000  iscmet3lem2  25334  iscmet3  25335  ivthlem1  25493  ivthlem2  25494  ivthlem3  25495  ovolfiniun  25543  volfiniun  25589  ioombl1lem4  25603  ismbf3d  25696  mbfi1flimlem  25764  itg2seq  25784  itgfsum  25869  ellimc3  25921  dvmptfsum  26017  c1liplem1  26038  plypf1  26252  plydivex  26338  aannenlem1  26369  ulmval  26420  ulmcau  26435  ulmbdd  26438  ulmcn  26439  ulmdvlem3  26442  sineq0  26566  efopn  26700  cxpeq  26799  logbgcd1irr  26836  rlimcnp  27007  xrlimcnp  27010  lgsdir2lem2  27367  lgsne0  27376  2lgsoddprm  27457  2sqlem6  27464  2sqlem10  27469  2sqreunnltblem  27492  ltsval2  27697  noetasuplem4  27777  conway  27849  madebdayim  27958  addsass  28075  oncutlt  28334  oniso  28341  addonbday  28349  n0ssoldg  28423  bdayn0p1  28439  oldfib  28447  bdaypw2n0bndlem  28533  bdayfinbndlem1  28537  z12bdaylem1  28540  z12zsodd  28552  axcontlem2  29112  uhgr0vb  29219  uvtx01vtx  29544  uvtxupgrres  29555  fusgrn0degnn0  29646  finsumvtxdg2size  29697  cusgrm1rusgr  29729  wlkv0  29796  wlklenvclwlk  29800  uspgrn2crct  29954  frrusgrord  30489  numclwwlk1lem2fo  30506  isgrpo  30646  grpoidinvlem3  30655  vcdi  30714  vcdir  30715  vcass  30716  nvs  30812  nvtri  30819  blocnilem  30953  chintcli  31480  hsupss  31490  shlej1  31509  elspansn4  31722  spansncvi  31801  hoaddsub  31965  lnopl  32063  lnfnl  32080  riesz4i  32212  pjnormssi  32317  pj3si  32356  stlei  32389  stcltr2i  32424  dmdmd  32449  dmdbr5  32457  mdslmd1lem2  32475  atssma  32527  atcvatlem  32534  chirredlem1  32539  atcvat4i  32546  mdsymlem2  32553  mdsymlem6  32557  sumdmdlem2  32568  cdjreui  32581  elimifd  32691  disjxpin  32737  xrge0infss  32912  expgt0b  32969  xrge0tsmsd  33214  gsumvsca1  33367  gsumvsca2  33368  lmxrge0  34210  ismeas  34457  eulerpartlemb  34626  bnj849  35184  bnj1110  35241  srcmpltd  35339  axprALT2  35369  trssfir1om  35371  fineqvinfep  35385  trssfir1omregs  35396  swrdrevpfx  35431  cusgredgex2  35437  subgrwlk  35446  cusgr3cyclex  35450  umgr2cycllem  35454  umgr2cycl  35455  connpconn  35549  cvmseu  35590  cvmliftlem15  35612  cvmlift2lem1  35616  cvmlift2lem12  35628  satfv0fun  35685  satffunlem  35715  mclsind  35884  r1peuqusdeg1  35957  dfon2lem3  36097  dfon2lem4  36098  dfon2lem6  36100  dfon2lem8  36102  dfon2lem9  36103  hbntg  36117  cgrdegen  36318  funtransport  36345  ifscgr  36358  cgrxfr  36369  brofs2  36391  brifs2  36392  idinside  36398  btwnconn1lem7  36407  btwnconn1lem11  36411  btwnconn1lem12  36412  btwnconn1lem14  36414  broutsideof2  36436  btwnoutside  36439  outsideoftr  36443  nmulprop  36504  in-ax8  36548  ss-ax8  36549  finminlem  36642  ntruni  36651  neibastop1  36683  ontgval  36755  ordtop  36760  ordcmp  36771  onint1  36773  bj-alrimdh  37031  bj-spimnfe  37060  bj-spimenfa  37061  bj-cbveximd  37068  bj-spvew  37072  bj-cbvexvv  37076  bj-ax12w  37114  axc11n11r  37122  bj-ax12v3  37124  bj-nnfan  37193  bj-nnfand  37194  bj-19.42t  37204  bj-sbft  37217  bj-nnflemea  37228  bj-hbaeb2  37267  bj-spcimdv  37344  bj-spcimdvv  37345  bj-sngltag  37432  bj-xtagex  37438  bj-axseprep  37523  bj-0int  37555  bj-ismooredr  37563  bj-inftyexpiinj  37665  nlpfvineqsn  37867  wl-ax13lem1  37952  wl-speqv  37989  wl-sbcom2d  38028  tan2h  38075  ptrest  38082  poimirlem20  38103  poimirlem22  38105  poimirlem26  38109  poimirlem30  38113  poimirlem31  38114  poimirlem32  38115  heicant  38118  voliunnfl  38127  volsupnfl  38128  itg2addnclem2  38135  itg2addnc  38137  itg2gt0cn  38138  ftc2nc  38165  filbcmb  38203  sdclem2  38205  seqpo  38210  nninfnub  38214  neificl  38216  prdstotbnd  38257  cnpwstotbnd  38260  heibor1lem  38272  heibor  38284  bfplem2  38286  opidonOLD  38315  exidu1  38319  grpokerinj  38356  rngoideu  38366  rngodi  38367  rngodir  38368  rngmgmbs4  38394  divrngidl  38491  prnc  38530  rsp3eq  38830  eqvrelqsel  39163  erimeq2  39226  prter2  39469  ax4fromc4  39482  hbae-o  39491  dvelimf-o  39517  ax12indn  39531  ax12inda2  39535  ax12a2-o  39538  l1cvpat  39642  atcvrj0  40016  pmaple  40349  paddasslem5  40412  pclfinN  40488  osumcllem11N  40554  pexmidlem8N  40565  dvheveccl  41700  dihord6apre  41844  lpolconN  42075  lcmineqlem1  42610  oexpreposd  42895  sn-it0e0  42989  cnreeu  43076  eu6w  43222  isnacs3  43255  pellexlem5  43374  pellex  43376  jm2.18  43529  jm2.15nn0  43544  jm2.16nn0  43545  dford3lem2  43568  ttac  43577  onexomgt  43782  onexoegt  43785  omabs2  43873  omcl3g  43875  tfsconcat0b  43887  naddgeoa  43935  safesnsupfiss  43955  rp-isfinite5  44057  cnvssb  44126  clcnvlem  44163  iunrelexpuztr  44259  rfovcnvf1od  44544  ntrrn  44662  nzss  44857  pm11.71  44937  axc11next  44946  hbntal  45093  eel2122old  45257  relwf  45507  modelaxreplem1  45518  ssclaxsep  45522  wfac8prim  45542  fsetsnf1  47610  2reu8i  47671  afvelima  47725  rlimdmafv  47735  rlimdmafv2  47816  elsprel  48045  sfprmdvdsmersenne  48176  perfectALTVlem2  48308  fpprwppr  48325  uhgrimedgi  48476  isuspgrim0lem  48479  uhgrimisgrgric  48517  gpgcubic  48665  gpg5nbgr3star  48667  pgnioedg1  48694  pgnioedg2  48695  pgnioedg3  48696  pgnioedg4  48697  pgnioedg5  48698  copisnmnd  48755  funcringcsetcALTV2lem8  48883  funcringcsetclem8ALTV  48906  lindslinindsimp2lem5  49048  nn0sumshdig  49209  prelrrx2b  49300  itscnhlc0yqe  49345  iscnrm3lem2  49520  diag1f1lem  49891  spd  50263  setrec1lem4  50275  setrec2fun  50277  aacllem  50386