Theorem syl6 35

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)

Hypotheses

Ref	Expression
syl6.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl6.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6

Step	Hyp	Ref	Expression
1		syl6.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6.2	. . 3 ⊢ (𝜒 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 3	sylcom 30	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  syl6com  37  a1dd  50  syl6mpi  67  syl6c  70  syl10  79  com34  91  con1d  145  expi  165  looinv  202  syl6ib  250  syl6ibr  251  syl6bi  252  syl6bir  253  jaoi  854  pm2.37  968  pm2.81  969  oplem1  1054  3jao  1424  impsingle  1630  al2im  1817  exlimdv  1937  19.23v  1946  19.36imvOLD  1950  spimfw  1970  ax13b  2036  nf5-1  2142  hbald  2169  19.8a  2175  spimedv  2191  19.9d  2197  sbequ1  2241  sbft  2263  cbv2w  2335  spimed  2389  cbv2  2404  cbv2h  2407  ax12  2424  axc11n  2427  equvini  2456  sb2  2481  sb4a  2485  mo3  2565  mopick  2628  moexexlem  2629  dvelimdc  2935  necon1ad  2961  necon4bd  2964  rsp2  3139  vtoclgft  3493  mo2icl  3650  2reu1  3831  reuss2  4250  reupick2  4255  elpwunsn  4620  pwpw0  4747  sssn  4760  pwsnOLD  4833  iuneqconst  4936  disjiun  5062  reusv1  5321  reusv3i  5328  ralxfrALT  5339  opth1  5391  copsexgw  5405  copsexg  5406  opelopabt  5446  solin  5529  wefrc  5584  frinxp  5670  ssrelrn  5806  reuop  6200  ordunidif  6318  oneqmini  6321  suctr  6353  ordsssuc2  6358  iotan0  6427  fv3  6801  ndmfv  6813  ssimaex  6862  fvopab3ig  6880  iinpreima  6955  fvcofneq  6978  dff3  6985  dff4  6986  ffnfv  7001  fnsnr  7046  fprb  7078  elunirn  7133  f1mpt  7143  isomin  7217  oprabidw  7315  oprabid  7316  mpoeq123  7356  sorpsscmpl  7596  dfwe2  7633  ssorduni  7638  ssonprc  7646  nlimsucg  7698  ordunisuc2  7700  tfinds  7715  ssnlim  7741  f1oweALT  7824  el2mpocl  7935  f1o2ndf1  7972  frxp  7976  soxp  7979  brtpos  8060  rntpos  8064  dftpos4  8070  onfununi  8181  onnseq  8184  smores2  8194  smo11  8204  tfr3  8239  rdglim2  8272  tz7.48lem  8281  tz7.49  8285  seqomlem2  8291  oawordex  8397  oa00  8399  oaass  8401  om00  8415  odi  8419  omass  8420  oeordi  8427  oelim2  8435  omsmo  8497  eroveu  8610  eceqoveq  8620  map0g  8681  fundmen  8830  sdomdif  8921  onsdominel  8922  pssnn  8960  nneneq  9001  php3  9004  nneneqOLD  9013  php3OLD  9016  onomeneqOLD  9021  pssnnOLD  9049  f1finf1o  9055  findcard3  9066  unblem1  9075  fiint  9100  ixpfi2  9126  dffi2  9191  elfiun  9198  fisup2g  9236  fiinf2g  9268  wemaplem2  9315  preleqALT  9384  inf3lem2  9396  inf3lem3  9397  inf3lem6  9400  noinfep  9427  epfrs  9498  tcmin  9508  r1sdom  9541  tz9.12lem3  9556  rankelb  9591  bndrank  9608  rankunb  9617  rankuni2b  9620  cplem1  9656  karden  9662  carduni  9748  infxpenlem  9778  dfac8alem  9794  alephdom  9846  cardinfima  9862  alephval3  9875  dfac5lem4  9891  dfac5lem5  9892  dfac5  9893  dfac2b  9895  kmlem13  9927  nnadju  9962  ackbij1b  10004  cfub  10014  coflim  10026  cflim2  10028  cfslbn  10032  cfslb2n  10033  cofsmo  10034  cfsmolem  10035  sornom  10042  fincssdom  10088  isf32lem1  10118  isf32lem2  10119  isf32lem9  10126  isf34lem4  10142  isfin1-3  10151  axcc4  10204  domtriomlem  10207  axdc2lem  10213  axdc3lem2  10216  zorn2lem4  10264  zorn2lem6  10266  zornn0g  10270  uniimadom  10309  cardmin  10329  ficard  10330  konigthlem  10333  alephreg  10347  cfpwsdom  10349  axextnd  10356  fpwwe2lem5  10400  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  canthp1lem2  10418  gchpwdom  10435  winalim2  10461  tskuni  10548  grupr  10562  grur1a  10584  axgroth6  10593  grothomex  10594  eltskm  10608  addclpi  10657  nqereu  10694  ltexnq  10740  nsmallnq  10742  genpn0  10768  genpss  10769  genpnmax  10772  ltaddpr  10799  reclem3pr  10814  reclem4pr  10815  suplem1pr  10817  supsrlem  10876  1re  10984  dedekindle  11148  addid1  11164  negn0  11413  negf1o  11414  negfi  11933  sup2  11940  supadd  11952  supmullem1  11954  supmullem2  11955  zmulcl  12378  zeo  12415  uz11  12616  uzwo  12660  eqreznegel  12683  lbzbi  12685  qextlt  12946  qextle  12947  xrsupsslem  13050  xrinfmsslem  13051  supxrun  13059  supxrpnf  13061  supxrunb1  13062  supxrunb2  13063  fzm1  13345  uzrdgfni  13687  hasheqf1oi  14075  hashreshashfun  14163  leisorel  14183  fundmge2nop0  14215  wrdsymb0  14261  swrdnnn0nd  14378  swrdccatin2d  14466  cshinj  14533  repswcshw  14534  rennim  14959  sqrlem6  14968  caubnd  15079  sqreulem  15080  caucvgrlem  15393  fsumcvg  15433  supcvg  15577  prodeq2ii  15632  fprodcvg  15649  prodmo  15655  dvdslelem  16027  bitsinv1lem  16157  bitsshft  16191  smuval2  16198  smupvallem  16199  gcdcllem1  16215  bezoutlem2  16257  bezoutlem3  16258  algcvga  16293  isprm3  16397  isprm5  16421  oddprmdvds  16613  vdwlem13  16703  vdwnnlem1  16705  vdwnnlem3  16707  ramub1lem1  16736  prmgaplem5  16765  imasaddfnlem  17248  divsfval  17267  catpropd  17427  joindmss  18106  meetdmss  18120  psdmrn  18300  odlem1  19152  gexlem1  19193  cygctb  19502  lmodfopnelem1  20168  islss  20205  lspsneq0  20283  lspsneq  20393  psgnodpmr  20804  obselocv  20944  mvrf1  21203  evlseu  21302  mpfrcl  21304  ppttop  22166  epttop  22168  elcls  22233  restntr  22342  cnprest  22449  regsep  22494  nrmsep3  22515  lmmo  22540  cmpsublem  22559  cmpsub  22560  hauscmplem  22566  txcnpi  22768  txcnp  22780  fbun  23000  fbfinnfr  23001  trfbas2  23003  fgcl  23038  filssufilg  23071  ufinffr  23089  isfcls  23169  fclsrest  23184  flimfnfcls  23188  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  alexsubALT  23211  cnextcn  23227  imasf1oxms  23654  metequiv2  23675  tngngpim  23832  iccpnfcnv  24116  iccpnfhmeo  24117  iscau2  24450  caun0  24454  minveclem3b  24601  itg1climres  24888  mbfi1fseqlem4  24892  ellimc3  25052  limccnp2  25065  dvlip  25166  itgsubstlem  25221  elply2  25366  coefv0  25418  coemulc  25425  ulmss  25565  sineq0  25689  scvxcvx  26144  sqf11  26297  ppiublem1  26359  fsumvma  26370  2sq2  26590  ostth  26796  mptelee  27272  brbtwn2  27282  colinearalg  27287  axcontlem4  27344  upgrres1  27689  usgr2trlncl  28137  umgrclwwlkge2  28364  upgr4cycl4dv4e  28558  1to3vfriendship  28654  3cyclfrgrrn1  28658  n4cyclfrgr  28664  frgrncvvdeqlem8  28679  frgrwopreg  28696  2clwwlk2clwwlk  28723  numclwwlk2lem1  28749  frgrreg  28767  frgrogt3nreg  28770  nmcvcn  29066  chlimi  29605  ocsh  29654  shsvs  29694  h1datomi  29952  stcl  30587  stge0  30595  stle1  30596  stm1addi  30616  stm1add3i  30618  cvnsym  30661  mdbr2  30667  dmdbr2  30674  mdsl0  30681  mdsl1i  30692  mdsl2i  30693  cvmdi  30695  atexch  30752  atcvat4i  30768  cdj1i  30804  xrge0iifcnv  31892  esumpr2  32044  sigaclci  32109  cntmeas  32203  mbfmcnt  32244  ballotlemfc0  32468  ballotlemfcc  32469  bnj1379  32819  bnj607  32905  bnj908  32920  bnj938  32926  bnj1174  32992  bnj1280  33009  f1resrcmplf1dlem  33067  fnrelpredd  33070  cusgr3cyclex  33107  loop1cycl  33108  acycgrislfgr  33123  pthacycspth  33128  iccllysconn  33221  satffunlem1lem1  33373  satfvel  33383  sate0fv0  33388  funpsstri  33748  fundmpss  33749  dfon2lem3  33770  dfon2lem4  33771  dfon2lem6  33773  dfon2lem9  33776  dfon2  33777  hbimtg  33791  hbaltg  33792  poxp2  33799  poxp3  33805  poseq  33811  sltres  33874  nosepdmlem  33895  nocvxminlem  33981  nocvxmin  33982  dfrdg4  34262  btwntriv2  34323  btwncomim  34324  btwnswapid  34328  btwnexch3  34331  ifscgr  34355  lineunray  34458  hilbert1.2  34466  cldbnd  34524  tailfb  34575  meran3  34611  arg-ax  34614  ontopbas  34626  onsuct0  34639  limsucncmpi  34643  ordcmp  34645  onint1  34647  bj-syl66ib  34744  bj-gl4  34786  bj-alexim  34817  bj-nfimt  34828  bj-ax6e  34858  bj-hbalt  34872  axc11n11r  34874  bj-nnfim  34937  bj-nnfan  34939  bj-nnfor  34941  bj-nnford  34942  bj-nnflemaa  34953  bj-nnflemae  34955  bj-19.21t  34960  bj-19.23t  34961  bj-19.42t  34964  bj-sbft  34966  bj-hbsb3t  34979  bj-cbv2hv  34988  bj-equsal1t  35014  bj-0int  35281  bj-bary1lem1  35491  topdifinffinlem  35527  isbasisrelowllem1  35535  isbasisrelowllem2  35536  iooelexlt  35542  finorwe  35562  finxpreclem1  35569  finxpreclem2  35570  isinf2  35585  fvineqsneu  35591  fvineqsneq  35592  pibt2  35597  wl-spae  35689  wl-19.8eqv  35691  wl-nfeqfb  35704  wl-mo3t  35740  wl-ax11-lem3  35747  fin2so  35773  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  ismblfin  35827  indexdom  35901  fzmul  35908  heibor1lem  35976  heibor  35988  exidu1  36023  rngoideu  36070  zerdivemp1x  36114  ispridl2  36205  cnf1dd  36257  cnf2dd  36258  cnfn1dd  36259  cnfn2dd  36260  orcomdd  36334  prtlem14  36895  prter2  36902  aev-o  36952  ax12eq  36962  ax12el  36963  ax12indn  36964  ax12indi  36965  lsatn0  37020  lsatcmp  37024  lsatcv0  37052  lfl1dim  37142  lfl1dim2N  37143  lkrss2N  37190  lub0N  37210  glb0N  37214  glbconxN  37399  hl2at  37426  cvrexchlem  37440  cvratlem  37442  cvrat4  37464  psubspi  37768  pointpsubN  37772  elpaddn0  37821  paddasslem17  37857  ispsubcl2N  37968  ldilval  38134  trlord  38590  diaelrnN  39066  cdlemm10N  39139  cdlemn11pre  39231  dihord2pre  39246  dihglblem2N  39315  dihglblem3N  39316  mapdrvallem2  39666  ioin9i8  40180  sn-dtru  40195  sn-sup2  40446  incssnn0  40540  fphpd  40645  rmxycomplete  40746  dford3lem1  40855  iocinico  41050  ensucne0OLD  41144  al3im  41262  brtrclfv2  41342  frege129d  41378  frege60a  41493  frege60c  41538  frege70  41548  rfovcnvf1od  41619  clsk1indlem3  41660  neik0pk1imk0  41664  gneispace  41751  gneispaceel2  41761  gneispacess2  41763  dvconstbi  41959  axc5c4c711toc7  42029  axc5c4c711to11  42030  pm14.24  42057  sbiota1  42059  bi33imp12  42117  bi123imp0  42123  ee233  42146  vk15.4j  42155  ssralv2  42158  alrim3con13v  42160  tratrb  42163  onfrALTlem3  42171  onfrALTlem2  42173  19.41rg  42177  hbimpg  42181  hbalg  42182  ax6e2ndeq  42186  e2  42258  ee223  42261  sspwtrALT  42449  sspwtrALT2  42450  suctrALT2  42464  trintALT  42508  isosctrlem1ALT  42561  fnchoice  42579  mptfnd  42793  stoweidlem62  43610  2reu8i  44616  2reuimp  44618  ffnafv  44674  lswn0  44907  reupr  44985  reuopreuprim  44989  requad2  45086  bgoldbnnsum3prm  45267  bgoldbtbndlem2  45269  bgoldbtbndlem4  45271  ply1mulgsumlem2  45739  iunord  46393  setrec2fun  46409