Theorem syl6 36

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 31	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  37  syl6com  38  a1dd  51  syl6mpi  68  syl6c  71  syl10  80  com34  92  con1d  146  expi  166  looinv  206  imbitrdi  254  imbitrrdi  255  biimtrdi  256  biimtrrdi  257  jaoi  870  pm2.37  986  pm2.81  987  oplem1  1070  3jao  1450  impsingle  1655  al2im  1842  exlimdv  1961  19.23v  1970  spimfw  1993  ax13b  2060  nf5-1  2178  hbald  2201  19.8a  2215  spimedv  2231  19.9d  2237  sbequ1  2282  sbft  2303  cbv2w  2367  spimed  2418  cbv2  2433  cbv2h  2436  ax12  2453  axc11n  2456  equvini  2485  sb2  2509  sb4a  2510  mo3  2590  mopick  2651  moexexlem  2652  dvelimdc  2947  necon1ad  2973  necon4bd  2976  rsp2  3280  mo2icl  3676  2reu1  3850  reuss2  4278  reupick2  4283  elpwunsn  4649  pwpw0  4778  sssn  4791  iuneqconst  4967  disjiun  5096  trun  5228  reusv1  5368  reusv3i  5375  ralxfrALT  5386  exneq  5417  opth1  5457  copsexgwOLD  5473  copsexg  5474  opelopabt  5516  solin  5596  wefrc  5655  frinxp  5744  ssrelrn  5884  dmcosseq  5968  dmcosseqOLD  5969  reuop  6294  ordunidif  6411  oneqmini  6414  suctr  6449  ordsssuc2  6454  iotan0  6526  fv3  6899  ndmfv  6913  ssimaex  6966  fvopab3ig  6985  iinpreima  7064  fvcofneq  7088  dff3  7095  dff4  7096  ffnfv  7114  fnsnr  7161  fprb  7192  elunirn  7249  f1mpt  7259  isomin  7335  oprabidw  7441  oprabid  7442  mpoeq123  7482  sorpsscmpl  7731  dfwe2  7772  ssorduni  7777  ssonprc  7785  nlimsucg  7837  ordunisuc2  7839  tfinds  7855  ssnlim  7881  f1oweALT  7968  mptcnfimad  7982  el2mpocl  8080  f1o2ndf1  8116  frxp  8121  soxp  8124  poxp2  8138  poxp3  8145  poseq  8153  brtpos  8230  rntpos  8234  dftpos4  8240  onfununi  8327  onnseq  8330  smores2  8340  smo11  8350  tfr3  8385  rdglim2  8418  tz7.48lem  8427  tz7.49  8431  seqomlem2  8437  oawordex  8541  oa00  8543  oaass  8545  om00  8559  odi  8563  omass  8564  oeordi  8572  oelim2  8580  omsmo  8643  eroveu  8809  eceqoveq  8819  map0g  8881  fundmen  9027  sdomdif  9112  onsdominel  9113  pssnn  9152  nneneq  9189  php3  9192  f1finf1o  9232  findcard3  9242  unblem1  9251  fiint  9285  ixpfi2  9306  dffi2  9382  elfiun  9389  fisup2g  9428  fiinf2g  9461  wemaplem2  9508  elirrv  9558  elirrvOLD  9559  preleqALT  9585  inf3lem2  9597  inf3lem3  9598  inf3lem6  9601  noinfep  9628  epfrs  9699  tcmin  9707  r1sdom  9745  tz9.12lem3  9760  rankelb  9795  bndrank  9812  rankunb  9821  rankuni2b  9824  cplem1  9874  karden  9880  carduni  9966  infxpenlem  9996  dfac8alem  10012  alephdom  10064  cardinfima  10080  alephval3  10093  dfac5lem4  10109  dfac5lem5  10110  dfac5  10111  dfac2b  10113  kmlem13  10145  nnadju  10180  ackbij1b  10220  cfub  10231  coflim  10244  cflim2  10246  cfslbn  10250  cfslb2n  10251  cofsmo  10252  cfsmolem  10253  sornom  10260  fincssdom  10306  isf32lem1  10336  isf32lem2  10337  isf32lem9  10344  isf34lem4  10360  isfin1-3  10369  axcc4  10422  domtriomlem  10425  axdc2lem  10431  axdc3lem2  10434  zorn2lem4  10482  zorn2lem6  10484  zornn0g  10488  uniimadom  10527  cardmin  10547  ficard  10548  konigthlem  10552  alephreg  10566  cfpwsdom  10568  axextnd  10575  fpwwe2lem5  10619  fpwwe2lem11  10625  fpwwe2lem12  10626  fpwwe2  10627  canthp1lem2  10637  gchpwdom  10654  winalim2  10680  tskuni  10767  grupr  10781  grur1a  10803  axgroth6  10812  grothomex  10813  eltskm  10827  addclpi  10876  nqereu  10913  ltexnq  10959  nsmallnq  10961  genpn0  10987  genpss  10988  genpnmax  10991  ltaddpr  11018  reclem3pr  11033  reclem4pr  11034  suplem1pr  11036  supsrlem  11095  1re  11207  dedekindle  11373  addrid  11389  negn0  11642  negf1o  11643  negfi  12163  sup2  12170  supadd  12182  supmullem1  12184  supmullem2  12185  zmulcl  12642  zeo  12681  uz11  12886  uzwo  12934  eqreznegel  12957  lbzbi  12959  qextlt  13228  qextle  13229  xrsupsslem  13332  xrinfmsslem  13333  supxrun  13341  supxrpnf  13343  supxrunb1  13344  supxrunb2  13345  fzm1  13635  uzrdgfni  13994  hasheqf1oi  14387  hashreshashfun  14476  leisorel  14497  fundmge2nop0  14539  wrdsymb0  14586  swrdnnn0nd  14694  swrdccatin2d  14781  cshinj  14848  repswcshw  14849  rennim  15290  01sqrexlem6  15298  caubnd  15410  sqreulem  15411  caucvgrlem  15724  fsumcvg  15763  supcvg  15910  prodeq2ii  15965  fprodcvg  15984  prodmo  15990  dvdslelem  16366  bitsinv1lem  16498  bitsshft  16532  smuval2  16539  smupvallem  16540  gcdcllem1  16556  bezoutlem2  16597  bezoutlem3  16598  algcvga  16636  isprm3  16740  isprm5  16765  oddprmdvds  16962  vdwlem13  17052  vdwnnlem1  17054  vdwnnlem3  17056  ramub1lem1  17085  prmgaplem5  17114  imasaddfnlem  17581  divsfval  17600  catpropd  17764  joindmss  18432  meetdmss  18446  psdmrn  18628  odlem1  19604  gexlem1  19648  cygctb  19961  rngisomring1  20549  lmodfopnelem1  20998  islss  21034  lspsneq0  21112  lspsneq  21225  psgnodpmr  21719  obselocv  21857  mvrf1  22114  evlseu  22213  mpfrcl  22215  ppttop  23143  epttop  23145  elcls  23209  restntr  23318  cnprest  23425  regsep  23470  nrmsep3  23491  lmmo  23516  cmpsublem  23535  cmpsub  23536  hauscmplem  23542  txcnpi  23744  txcnp  23756  fbun  23976  fbfinnfr  23977  trfbas2  23979  fgcl  24014  filssufilg  24047  ufinffr  24065  isfcls  24145  fclsrest  24160  flimfnfcls  24164  alexsubALTlem2  24184  alexsubALTlem3  24185  alexsubALTlem4  24186  alexsubALT  24187  cnextcn  24203  imasf1oxms  24625  metequiv2  24646  tngngpim  24795  iccpnfcnv  25082  iccpnfhmeo  25083  iscau2  25415  caun0  25419  minveclem3b  25566  itg1climres  25852  mbfi1fseqlem4  25856  ellimc3  26017  limccnp2  26030  dvlip  26131  itgsubstlem  26186  elply2  26332  coefv0  26384  coemulc  26391  ulmss  26536  sineq0  26665  scvxcvx  27126  sqf11  27279  ppiublem1  27342  fsumvma  27353  2sq2  27573  ostth  27779  ltsres  27802  nosepdmlem  27823  nobdaymin  27922  nocvxminlem  27923  addsprop  28145  mpteleeOLD  29211  brbtwn2  29221  colinearalg  29226  axcontlem4  29283  upgrres1  29629  usgr2trlncl  30075  umgrclwwlkge2  30308  upgr4cycl4dv4e  30502  1to3vfriendship  30598  3cyclfrgrrn1  30602  n4cyclfrgr  30608  frgrncvvdeqlem8  30623  frgrwopreg  30640  2clwwlk2clwwlk  30667  numclwwlk2lem1  30693  frgrreg  30711  frgrogt3nreg  30714  nmcvcn  31013  chlimi  31552  ocsh  31601  shsvs  31641  h1datomi  31899  stcl  32534  stge0  32542  stle1  32543  stm1addi  32563  stm1add3i  32565  cvnsym  32608  mdbr2  32614  dmdbr2  32621  mdsl0  32628  mdsl1i  32639  mdsl2i  32640  cvmdi  32642  atexch  32699  atcvat4i  32715  cdj1i  32751  1arithufdlem4  33803  xrge0iifcnv  34289  esumpr2  34423  sigaclci  34488  cntmeas  34582  mbfmcnt  34624  ballotlemfc0  34849  ballotlemfcc  34850  bnj1379  35184  bnj607  35270  bnj908  35285  bnj938  35291  bnj1174  35357  bnj1280  35374  f1resrcmplf1dlem  35440  fnrelpredd  35448  r1filimi  35463  fineqvinfep  35504  tz9.1regs  35513  axsepg2  35519  axsepg4  35522  axnulg  35524  axpowg2  35526  axpowg3  35527  kardcard2b  35544  ackardcard  35546  cusgr3cyclex  35594  loop1cycl  35595  acycgrislfgr  35610  pthacycspth  35615  iccllysconn  35708  satffunlem1lem1  35860  satfvel  35870  sate0fv0  35875  antnestlaw2  36150  funpsstri  36224  fundmpss  36225  dfon2lem3  36241  dfon2lem4  36242  dfon2lem6  36244  dfon2lem9  36247  dfon2  36248  hbimtg  36262  hbaltg  36263  dfrdg4  36409  btwntriv2  36470  btwncomim  36471  btwnswapid  36475  btwnexch3  36478  ifscgr  36502  lineunray  36605  hilbert1.2  36613  cldbnd  36803  tailfb  36854  meran3  36890  arg-ax  36893  ontopbas  36905  onsuct0  36918  limsucncmpi  36922  ordcmp  36924  onint1  36926  weiunpo  36942  axtcond  36955  axuntco  36956  dfttc4lem2  37006  bj-bisimpl  37111  bj-bisimpr  37112  bj-syl66ib  37113  bj-gl4  37154  bj-alexim  37199  bj-nfimt  37211  bj-spvw  37223  bj-cbvalvv  37227  bj-ax6e  37256  bj-hbald  37270  axc11n11r  37274  bj-nnfim  37343  bj-nnfan  37345  bj-nnfor  37347  bj-nnford  37348  bj-19.21t  37352  bj-19.23t  37353  bj-19.42t  37356  bj-sbft  37369  bj-nnflemaa  37377  bj-nnflemae  37379  bj-hbsb3t  37389  bj-cbv2hv  37398  bj-equsal1t  37423  bj-axreprepsep  37678  bj-0int  37709  bj-bary1lem1  37921  topdifinffinlem  37959  isbasisrelowllem1  37967  isbasisrelowllem2  37968  iooelexlt  37974  finorwe  37994  finxpreclem1  38001  finxpreclem2  38002  isinf2  38017  fvineqsneu  38023  fvineqsneq  38024  pibt2  38029  wl-spae  38142  wl-19.8eqv  38144  wl-nfeqfb  38157  wl-mo3t  38197  wl-eujustlem1  38209  fin2so  38224  poimirlem29  38266  poimirlem30  38267  poimirlem31  38268  poimirlem32  38269  ismblfin  38278  indexdom  38351  fzmul  38358  heibor1lem  38426  heibor  38438  exidu1  38473  rngoideu  38520  zerdivemp1x  38564  ispridl2  38655  cnf1dd  38707  cnf2dd  38708  cnfn1dd  38709  cnfn2dd  38710  orcomdd  38784  disjlem14  39518  disjdmqsss  39522  disjdmqscossss  39523  prtlem14  39616  prter2  39623  aev-o  39673  ax12eq  39683  ax12el  39684  ax12indn  39685  ax12indi  39686  lsatn0  39741  lsatcmp  39745  lsatcv0  39773  lfl1dim  39863  lfl1dim2N  39864  lkrss2N  39911  lub0N  39931  glb0N  39935  glbconxN  40120  hl2at  40147  cvrexchlem  40161  cvratlem  40163  cvrat4  40185  psubspi  40489  pointpsubN  40493  elpaddn0  40542  paddasslem17  40578  ispsubcl2N  40689  ldilval  40855  trlord  41311  diaelrnN  41787  cdlemm10N  41860  cdlemn11pre  41952  dihord2pre  41967  dihglblem2N  42036  dihglblem3N  42037  mapdrvallem2  42387  ioin9i8  42944  sn-sup2  43233  incssnn0  43412  fphpd  43513  rmxycomplete  43614  dford3lem1  43723  iocinico  43909  onsupnmax  43925  cantnfresb  44021  cantnf2  44022  tfsconcatb0  44041  tfsconcat0b  44043  sdomne0  44109  sdomne0d  44110  ensucne0OLD  44226  al3im  44343  brtrclfv2  44423  frege129d  44459  frege60a  44574  frege60c  44619  frege70  44629  rfovcnvf1od  44700  clsk1indlem3  44739  neik0pk1imk0  44743  gneispace  44830  gneispaceel2  44840  gneispacess2  44842  dvconstbi  45014  axc5c4c711toc7  45084  axc5c4c711to11  45085  pm14.24  45112  sbiota1  45114  bi33imp12  45170  bi123imp0  45175  ee233  45198  vk15.4j  45207  ssralv2  45210  alrim3con13v  45212  tratrb  45215  onfrALTlem3  45223  onfrALTlem2  45225  19.41rg  45229  hbimpg  45233  hbalg  45234  ax6e2ndeq  45238  e2  45310  ee223  45313  sspwtrALT  45500  sspwtrALT2  45501  suctrALT2  45515  trintALT  45559  isosctrlem1ALT  45612  relpmin  45631  traxext  45656  modelaxreplem2  45658  ssclaxsep  45661  fnchoice  45719  mptfnd  45927  stoweidlem62  46746  2reu8i  47817  2reuimp  47819  ffnafv  47875  lswn0  48160  reupr  48238  reuopreuprim  48242  requad2  48355  bgoldbnnsum3prm  48536  bgoldbtbndlem2  48538  bgoldbtbndlem4  48540  gricsym  48653  gpgedgvtx1  48794  ply1mulgsumlem2  49134  iunord  50421  setrec2fun  50437