Theorem sylan 283

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

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

Assertion

Ref	Expression
sylan	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylan.2	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
3	2	expcom 116	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	mpan9 281	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  sylanb  284  sylanbr  285  syl2an  289  sylanl1  402  sylanl2  403  mpanl1  434  mpanl2  435  syldanl  449  adantll  476  adantlr  477  ancom1s  569  pm4.55dc  944  dfifp2dc  987  3adantl1  1177  3adantl2  1178  3adantl3  1179  syl3anl1  1319  syl3anl3  1321  syl3anl  1322  stoic3  1473  eupick  2157  csbiebt  3165  csbnestgf  3178  reuss2  3485  mpteq12  4170  otexg  4320  opelopabt  4354  sonr  4412  sotr  4413  issod  4414  so2nr  4416  so3nr  4417  ordelss  4474  onelon  4479  elrnmpt1s  4980  iota2  5314  funeu  5349  imadif  5407  fnbr  5431  feu  5516  f1ss  5545  f1ssres  5548  f1resf1  5549  dffo2  5560  foco  5567  foun  5599  fun11iun  5601  ffoss  5612  funbrfv  5678  fvco3  5713  fvopab6  5739  funfvbrb  5756  elpreima  5762  ffvelcdm  5776  ffvelcdmda  5778  dffo4  5791  fmptco  5809  fsn2  5817  fncofn  5827  fvconst2g  5863  fex  5878  funfvima  5881  f1elima  5909  f1ocnvfv1  5913  f1ocnvfv2  5914  cocan2  5924  foeqcnvco  5926  isocnv  5947  isores2  5949  isoini  5954  isoselem  5956  f1oiso  5962  f1ofveu  6001  eloprabga  6103  suppssof1  6248  ofco  6249  offveqb  6250  ofc1g  6252  ofc2g  6253  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  fnexALT  6268  f1dmex  6273  ot1stg  6310  ot2ndg  6311  ot3rdgg  6312  eqopi  6330  2ndrn  6341  fo2ndf  6387  smores3  6454  smores2  6455  smoel  6461  smoiso  6463  tfrlem1  6469  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemiubacc  6491  tfr1onlemsucaccv  6502  tfr1onlembfn  6505  tfr1onlemubacc  6507  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucaccv  6515  tfrcllembfn  6518  tfrcllemubacc  6520  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  frecrdg  6569  omv2  6628  nnasuc  6639  nnmsuc  6640  nnacom  6647  nnaass  6648  nnmass  6650  nntri1  6659  nndifsnid  6670  nnmordi  6679  swoer  6725  erth  6743  riinerm  6772  qliftlem  6777  ecovass  6808  ecoviass  6809  elmapssres  6837  fvixp  6867  f1domg  6926  domssr  6946  endomtr  6959  xpsnen2g  7008  enen1  7021  enen2  7022  domen1  7023  domen2  7024  mapen  7027  mapxpen  7029  ssenen  7032  phplem1  7033  fidifsnid  7053  findcard  7072  findcard2  7073  findcard2s  7074  fidcen  7083  fieq0  7169  isotilem  7199  supisolem  7201  inflbti  7217  ordiso2  7228  djuex  7236  updjudhcoinlf  7273  updjudhcoinrg  7274  updjud  7275  ctssdccl  7304  enumctlemm  7307  nnnninf  7319  finomni  7333  pm54.43  7389  acfun  7415  ccfunen  7476  cc2lem  7478  cc3  7480  addclpi  7540  addasspig  7543  mulasspig  7545  addnidpig  7549  nnppipi  7556  ltanqi  7615  ltmnqi  7616  ltexnqq  7621  archnqq  7630  prarloclemarch2  7632  enq0sym  7645  enq0tr  7647  nqnq0pi  7651  nqnq0  7654  mulcanenq0ec  7658  addclnq0  7664  nqpnq0nq  7666  distrnq0  7672  addassnq0lemcl  7674  addassnq0  7675  prubl  7699  prarloclemlt  7706  genpdf  7721  genipv  7722  genpelvl  7725  genpelvu  7726  genpml  7730  genpmu  7731  genprndl  7734  genprndu  7735  genpassl  7737  genpassu  7738  genpassg  7739  addnqprl  7742  addnqpru  7743  addlocpr  7749  nqprm  7755  nqprl  7764  nqpru  7765  mulnqprl  7781  mulnqpru  7782  mullocprlem  7783  mullocpr  7784  addcomprg  7791  mulcomprg  7793  distrlem1prl  7795  distrlem1pru  7796  distrlem4prl  7797  distrlem4pru  7798  ltprordil  7802  1idprl  7803  1idpru  7804  ltpopr  7808  ltsopr  7809  ltaddpr  7810  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemlol  7815  ltexprlemopu  7816  ltexprlemupu  7817  ltexprlemdisj  7819  ltexprlemloc  7820  ltexprlemfl  7822  ltexprlemrl  7823  ltexprlemfu  7824  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  prplnqu  7833  recexprlemloc  7844  recexprlem1ssl  7846  recexprlem1ssu  7847  recexprlemss1l  7848  recexprlemss1u  7849  aptiprleml  7852  aptiprlemu  7853  cauappcvgprlemloc  7865  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  caucvgprlemloc  7888  caucvgprlemladdrl  7891  caucvgprprlemml  7907  caucvgprprlemloc  7916  00sr  7982  map2psrprg  8018  suplocsrlempr  8020  suplocsrlem  8021  adddir  8163  axsuploc  8245  eqle  8264  le2tri3i  8281  mul4  8304  muladd11  8305  cnegexlem3  8349  addsub12  8385  2addsub  8386  addsubeq4  8387  subadd4  8416  negcon1  8424  negdi2  8430  negsubdi2  8431  neg2sub  8432  renegcl  8433  muladd  8556  subdir  8558  gt0ne0  8600  ltnegcon1  8636  lenegcon1  8639  eqord1  8656  eqord2  8657  recexre  8751  ltmul1  8765  recexap  8826  div12ap  8867  rerecapb  9016  p1le  9022  ltmul2  9029  gt0div  9043  ge0div  9044  zlem1lt  9529  nnaddm1cl  9534  zdceq  9548  gtndiv  9568  prime  9572  msqznn  9573  btwnz  9592  uzss  9770  eluzadd  9778  nn0pzuz  9814  supinfneg  9822  infsupneg  9823  divfnzn  9848  qnegcl  9863  qreccl  9869  elpqb  9877  xaddass  10097  xleadd1a  10101  xlesubadd  10111  elico2  10165  iccss  10169  iccsupr  10194  elfz5  10245  fznn  10317  difelfznle  10363  fzoaddel  10425  elincfzoext  10431  qdceq  10497  qbtwnxr  10510  flqbi2  10544  adddivflid  10545  fldivnn0  10548  divfl0  10549  flqmulnn0  10552  fldivnn0le  10556  fldiv4p1lem1div2  10558  ceiqle  10568  flqdiv  10576  modqmulnn  10597  frecuzrdgtcl  10667  frecuzrdgsuc  10669  frecuzrdgdomlem  10672  frecuzrdgfunlem  10674  frecuzrdgsuctlem  10678  seqm1g  10729  seq3caopr2  10748  seqcaopr2g  10749  iseqf1olemkle  10752  seq3f1olemp  10770  seqf1oglem2  10775  seqf1og  10776  seq3id  10780  seq3z  10783  expap0  10824  mulexp  10833  mulexpzap  10834  expmul  10839  leexp1a  10849  expubnd  10851  zesq  10913  bernneq  10915  bernneq3  10917  modqexp  10921  facdiv  10993  facndiv  10994  faclbnd3  10998  faclbnd6  10999  bccmpl  11009  bcpasc  11021  bccl  11022  seq3coll  11099  fundm2domnop  11103  wrdsymb1  11143  ccatfv0  11173  ccatrn  11179  ccat2s1cl  11203  lswccats1fst  11214  swrdspsleq  11241  pfxtrcfv  11267  pfxsuffeqwrdeq  11272  pfxlswccat  11287  wrdeqs1cat  11294  cats1un  11295  swrdccatin1  11299  pfxccatin12lem4  11300  swrdccatin2  11303  pfxccatin12  11307  swrdccat  11309  shftlem  11370  ovshftex  11373  shftval4  11382  shftf  11384  shftcan2  11389  crim  11412  mulreap  11418  remul2  11427  immul2  11434  cjexp  11447  caucvgre  11535  r19.2uz  11547  sqrtsq2  11597  absnid  11627  absexp  11633  nn0abscl  11639  abslt  11642  lenegsq  11649  cau3lem  11668  minmax  11784  xrmaxadd  11815  clim  11835  climshftlemg  11856  climcn1  11862  climcn1lem  11873  clim2ser  11891  clim2ser2  11892  iserex  11893  isermulc2  11894  climub  11898  climcaucn  11905  serf0  11906  summodclem3  11934  summodclem2a  11935  summodclem2  11936  summodc  11937  fsum3  11941  fsumf1o  11944  fisumss  11946  isumss2  11947  fsumcl2lem  11952  fsumadd  11960  fsumsplit  11961  isummulc2  11980  fsum2d  11989  fsummulc2  12002  telfsumo  12020  fsumparts  12024  hash2iun1dif1  12034  bcxmas  12043  isumshft  12044  isumsplit  12045  expcnvap0  12056  geolim  12065  geolim2  12066  cvgratnnlemmn  12079  cvgratnnlemseq  12080  mertenslemi1  12089  mertenslem2  12090  mertensabs  12091  clim2divap  12094  prodmodclem3  12129  prodmodclem2a  12130  fprodseq  12137  fprodf1o  12142  fprodmul  12145  fprodsplitdc  12150  efcllemp  12212  reefcl  12222  efcj  12227  efaddlem  12228  efexp  12236  reeftlcl  12243  eftlub  12244  efsep  12245  effsumlt  12246  eflegeo  12255  retanclap  12276  demoivre  12327  demoivreALT  12328  eirraplem  12331  dvdsval3  12345  p1modz1  12348  iddvdsexp  12369  alzdvds  12408  addmodlteqALT  12413  nnehalf  12458  nno  12460  ndvdsadd  12485  bitsp1e  12506  bitsp1o  12507  bitsinv1  12516  divgcdnnr  12540  neggcd  12547  gcdabs  12552  bezoutlemmain  12562  bezoutlemaz  12567  bezoutlembz  12568  gcdmultiplez  12585  gcdzeq  12586  dvdssq  12595  nninfctlemfo  12604  algrf  12610  algcvg  12613  algcvga  12616  algfx  12617  eucalgf  12620  eucalgcvga  12623  neglcm  12640  lcmabs  12641  lcmdvds  12644  lcmgcdeq  12648  qredeq  12661  isprm3  12683  coprm  12709  prmrp  12710  isprm6  12712  prmdvdsexpb  12714  rpexp  12718  cncongrprm  12722  sqrt2irraplemnn  12744  phibndlem  12781  phiprmpw  12787  eulerthlemh  12796  eulerthlemth  12797  fermltl  12799  prmdivdiv  12802  modprm1div  12813  m1dvdsndvds  12814  coprimeprodsq  12823  pczpre  12863  pczcl  12864  pcexp  12875  pczdvds  12880  pczndvds  12882  pczndvds2  12884  pcdvdsb  12886  pcneg  12891  pcprmpw  12900  difsqpwdvds  12904  pcmptcl  12908  pcprod  12912  fldivp1  12914  infpnlem2  12926  1arithlem4  12932  ennnfonelemrn  13033  topnidg  13328  pwselbasb  13369  pwsplusgval  13371  pwsmulrval  13372  imasaddfnlemg  13390  imasaddflemg  13392  qusin  13402  mgmlrid  13455  mndass  13500  prdsidlem  13523  mhmco  13566  gsumsubm  13570  gsumwcl  13573  gsumwmhm  13574  grpass  13585  grpinvex  13586  dfgrp2  13603  grplid  13607  grprid  13608  grprcan  13613  grpinvssd  13653  grpinvval2  13659  prdsinvlem  13684  pwsinvg  13688  mhmid  13695  mhmmnd  13696  ghmgrp  13698  mulgnn  13706  mulgnnp1  13710  mulgnegnn  13712  mulgnnsubcl  13714  mulgz  13730  issubg2m  13769  issubg4m  13773  subgintm  13778  nmzbi  13789  eqger  13804  eqgid  13806  eqgen  13807  qusgrp  13812  qusadd  13814  qusinv  13816  qussub  13817  ghminv  13830  ghmsub  13831  ghmrn  13837  resghm2b  13842  ghmf1  13853  conjsubg  13857  conjsubgen  13858  qusghm  13862  cmncom  13882  ablsubadd  13892  ablsubsub23  13905  ghmcmn  13907  gsumfzreidx  13917  mgpress  13937  srg1expzeq1  14001  ringinvnz1ne0  14055  ringinvnzdiv  14056  dvdsrd  14101  dvdsunit  14119  unitinvcl  14130  unitinvinv  14131  unitlinv  14133  unitrinv  14134  rhmunitinv  14185  subrngintm  14219  subrg1  14238  subrguss  14243  subrginv  14244  subrgunit  14246  subrgugrp  14247  subrgintm  14250  resrhm  14255  resrhm2b  14256  lmodass  14310  lmodlcan  14311  lmod0vlid  14325  lmod0vrid  14326  lmod0vid  14327  lmodvs0  14329  lcomf  14334  lmodvnegcl  14335  lmodvnegid  14336  lmodvsubadd  14345  lmodsubid  14354  lss1d  14390  lspval  14397  lspsnel6  14415  lspsnneg  14427  sralmod  14457  dflidl2rng  14488  lidlacl  14491  dflidl2  14495  df2idl2  14516  qusmul2  14536  quscrng  14540  cnfldmulg  14583  znf1o  14658  znidom  14664  psraddcl  14687  psr0lid  14689  tgss3  14795  clsval  14828  clsss3  14847  neiss2  14859  resttop  14887  resttopon2  14895  lmconst  14933  cnima  14937  cnntri  14941  cncnp  14947  cnrest  14952  cndis  14958  lmss  14963  lmff  14966  lmtopcnp  14967  txcnp  14988  upxp  14989  uptx  14991  cnmpt11  15000  hmeoima  15027  hmeoopn  15028  hmeocld  15029  hmeontr  15030  hmeoimaf1o  15031  mettri2  15079  met0  15081  metres2  15098  blpnf  15117  xblss2ps  15121  xblss2  15122  blbas  15150  blres  15151  xmetec  15154  mopnss  15167  xmstri2  15187  mstri2  15188  xmstri  15189  mstri  15190  xmstri3  15191  mstri3  15192  msrtri  15193  mopni3  15201  unimopn  15203  comet  15216  bdxmet  15218  climcncf  15301  dedekindeulemuub  15334  dedekindicclemuub  15343  ivthdichlem  15368  dvfgg  15405  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvfre  15427  dvmptfsum  15442  plyadd  15468  plymul  15469  reeff1olem  15488  reeff1o  15490  sinperlem  15525  abssinper  15563  reexplog  15588  relogexp  15589  cxpexpnn  15613  cxprec  15627  rpcxpmul2  15630  abscxp  15632  wilthlem1  15697  sgmval2  15701  sgmnncl  15705  0sgmppw  15710  perfectlem1  15716  lgsdir  15757  lgsprme0  15764  lgsdinn0  15770  gausslemma2dlem3  15785  gausslemma2dlem5a  15787  2lgslem1a2  15809  2lgslem1a  15810  2lgslem3  15823  2lgs  15826  umgredgprv  15959  umgrislfupgrdom  15975  uspgredgiedg  16022  uspgriedgedg  16023  usgrislfuspgrdom  16034  usgredg2en  16039  usgredgprv  16040  usgrpredgv  16042  usgredg  16044  usgrnloopv  16045  usgredgne  16048  usgredg3  16058  usgredgedg  16071  usgredgdomord  16074  usgr1vr  16092  umgrwlknloop  16179  wlkres  16188  clwwlkccatlem  16209  clwwlkccat  16210  bj-inex  16452  bj-nn0suc  16509  bj-nn0sucALT  16523  trilpolemeq1  16594  trilpolemlt1  16595  trirec0  16598  nconstwlpolemgt0  16618