Theorem sylan 281

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 115	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	mpan9 279	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylanb  282  sylanbr  283  syl2an  287  sylanl1  400  sylanl2  401  mpanl1  431  mpanl2  432  adantll  468  adantlr  469  ancom1s  559  3adantl1  1143  3adantl2  1144  3adantl3  1145  syl3anl1  1276  syl3anl3  1278  syl3anl  1279  stoic3  1419  eupick  2093  csbiebt  3083  csbnestgf  3096  reuss2  3401  mpteq12  4064  otexg  4207  opelopabt  4239  sonr  4294  sotr  4295  issod  4296  so2nr  4298  so3nr  4299  ordelss  4356  onelon  4361  elrnmpt1s  4853  iota2  5178  funeu  5212  imadif  5267  fnbr  5289  feu  5369  f1ss  5398  f1ssres  5401  f1resf1  5402  dffo2  5413  foco  5419  foun  5450  fun11iun  5452  ffoss  5463  funbrfv  5524  fvco3  5556  fvopab6  5581  funfvbrb  5597  elpreima  5603  ffvelrn  5617  ffvelrnda  5619  dffo4  5632  fmptco  5650  fsn2  5658  fvconst2g  5698  fex  5713  funfvima  5715  f1elima  5740  f1ocnvfv1  5744  f1ocnvfv2  5745  cocan2  5755  foeqcnvco  5757  isocnv  5778  isores2  5780  isoini  5785  isoselem  5787  f1oiso  5793  f1ofveu  5829  eloprabga  5925  grprinvlem  6032  suppssof1  6066  ofco  6067  offveqb  6068  fnexALT  6078  f1dmex  6081  ot1stg  6117  ot2ndg  6118  ot3rdgg  6119  eqopi  6137  2ndrn  6148  fo2ndf  6191  smores3  6257  smores2  6258  smoel  6264  smoiso  6266  tfrlem1  6272  tfrlemisucaccv  6289  tfrlemibxssdm  6291  tfrlemiubacc  6294  tfr1onlemsucaccv  6305  tfr1onlembfn  6308  tfr1onlemubacc  6310  tfr1onlemaccex  6312  tfr1onlemres  6313  tfrcllemsucaccv  6318  tfrcllembfn  6321  tfrcllemubacc  6323  tfrcllemaccex  6325  tfrcllemres  6326  tfrcl  6328  frecrdg  6372  omv2  6429  nnasuc  6440  nnmsuc  6441  nnacom  6448  nnaass  6449  nnmass  6451  nntri1  6460  nndifsnid  6471  nnmordi  6480  swoer  6525  erth  6541  riinerm  6570  qliftlem  6575  ecovass  6606  ecoviass  6607  elmapssres  6635  fvixp  6665  f1domg  6720  endomtr  6752  xpsnen2g  6791  enen1  6802  enen2  6803  domen1  6804  domen2  6805  mapen  6808  mapxpen  6810  ssenen  6813  phplem1  6814  fidifsnid  6833  findcard  6850  findcard2  6851  findcard2s  6852  fieq0  6937  isotilem  6967  supisolem  6969  inflbti  6985  ordiso2  6996  djuex  7004  updjudhcoinlf  7041  updjudhcoinrg  7042  updjud  7043  ctssdccl  7072  enumctlemm  7075  nnnninf  7086  finomni  7100  pm54.43  7142  acfun  7159  ccfunen  7201  cc2lem  7203  cc3  7205  addclpi  7264  addasspig  7267  mulasspig  7269  addnidpig  7273  nnppipi  7280  ltanqi  7339  ltmnqi  7340  ltexnqq  7345  archnqq  7354  prarloclemarch2  7356  enq0sym  7369  enq0tr  7371  nqnq0pi  7375  nqnq0  7378  mulcanenq0ec  7382  addclnq0  7388  nqpnq0nq  7390  distrnq0  7396  addassnq0lemcl  7398  addassnq0  7399  prubl  7423  prarloclemlt  7430  genpdf  7445  genipv  7446  genpelvl  7449  genpelvu  7450  genpml  7454  genpmu  7455  genprndl  7458  genprndu  7459  genpassl  7461  genpassu  7462  genpassg  7463  addnqprl  7466  addnqpru  7467  addlocpr  7473  nqprm  7479  nqprl  7488  nqpru  7489  mulnqprl  7505  mulnqpru  7506  mullocprlem  7507  mullocpr  7508  addcomprg  7515  mulcomprg  7517  distrlem1prl  7519  distrlem1pru  7520  distrlem4prl  7521  distrlem4pru  7522  ltprordil  7526  1idprl  7527  1idpru  7528  ltpopr  7532  ltsopr  7533  ltaddpr  7534  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemlol  7539  ltexprlemopu  7540  ltexprlemupu  7541  ltexprlemdisj  7543  ltexprlemloc  7544  ltexprlemfl  7546  ltexprlemrl  7547  ltexprlemfu  7548  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  prplnqu  7557  recexprlemloc  7568  recexprlem1ssl  7570  recexprlem1ssu  7571  recexprlemss1l  7572  recexprlemss1u  7573  aptiprleml  7576  aptiprlemu  7577  cauappcvgprlemloc  7589  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  caucvgprlemloc  7612  caucvgprlemladdrl  7615  caucvgprprlemml  7631  caucvgprprlemloc  7640  00sr  7706  map2psrprg  7742  suplocsrlempr  7744  suplocsrlem  7745  adddir  7886  axsuploc  7967  eqle  7986  le2tri3i  8003  mul4  8026  muladd11  8027  cnegexlem3  8071  addsub12  8107  2addsub  8108  addsubeq4  8109  subadd4  8138  negcon1  8146  negdi2  8152  negsubdi2  8153  neg2sub  8154  renegcl  8155  muladd  8278  subdir  8280  gt0ne0  8321  ltnegcon1  8357  lenegcon1  8360  eqord1  8377  eqord2  8378  recexre  8472  ltmul1  8486  recexap  8546  div12ap  8586  p1le  8740  ltmul2  8747  gt0div  8761  ge0div  8762  zlem1lt  9243  nnaddm1cl  9248  zdceq  9262  gtndiv  9282  prime  9286  msqznn  9287  btwnz  9306  uzss  9482  eluzadd  9490  nn0pzuz  9521  supinfneg  9529  infsupneg  9530  divfnzn  9555  qnegcl  9570  qreccl  9576  elpqb  9583  xaddass  9801  xleadd1a  9805  xlesubadd  9815  elico2  9869  iccss  9873  iccsupr  9898  elfz5  9948  fznn  10020  difelfznle  10066  fzoaddel  10123  qdceq  10178  qbtwnxr  10189  flqbi2  10222  adddivflid  10223  fldivnn0  10226  divfl0  10227  flqmulnn0  10230  fldivnn0le  10234  fldiv4p1lem1div2  10236  ceiqle  10244  flqdiv  10252  modqmulnn  10273  frecuzrdgtcl  10343  frecuzrdgsuc  10345  frecuzrdgdomlem  10348  frecuzrdgfunlem  10350  frecuzrdgsuctlem  10354  seq3caopr2  10413  iseqf1olemkle  10415  seq3f1olemp  10433  seq3id  10439  seq3z  10442  expap0  10481  mulexp  10490  mulexpzap  10491  expmul  10496  leexp1a  10506  expubnd  10508  zesq  10569  bernneq  10571  bernneq3  10573  modqexp  10577  facdiv  10647  facndiv  10648  faclbnd3  10652  faclbnd6  10653  bccmpl  10663  bcpasc  10675  bccl  10676  seq3coll  10751  shftlem  10754  ovshftex  10757  shftval4  10766  shftf  10768  shftcan2  10773  crim  10796  mulreap  10802  remul2  10811  immul2  10818  cjexp  10831  caucvgre  10919  r19.2uz  10931  sqrtsq2  10981  absnid  11011  absexp  11017  nn0abscl  11023  abslt  11026  lenegsq  11033  cau3lem  11052  minmax  11167  xrmaxadd  11198  clim  11218  climshftlemg  11239  climcn1  11245  climcn1lem  11256  clim2ser  11274  clim2ser2  11275  iserex  11276  isermulc2  11277  climub  11281  climcaucn  11288  serf0  11289  summodclem3  11317  summodclem2a  11318  summodclem2  11319  summodc  11320  fsum3  11324  fsumf1o  11327  fisumss  11329  isumss2  11330  fsumcl2lem  11335  fsumadd  11343  fsumsplit  11344  isummulc2  11363  fsum2d  11372  fsummulc2  11385  telfsumo  11403  fsumparts  11407  hash2iun1dif1  11417  bcxmas  11426  isumshft  11427  isumsplit  11428  expcnvap0  11439  geolim  11448  geolim2  11449  cvgratnnlemmn  11462  cvgratnnlemseq  11463  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  clim2divap  11477  prodmodclem3  11512  prodmodclem2a  11513  fprodseq  11520  fprodf1o  11525  fprodmul  11528  fprodsplitdc  11533  efcllemp  11595  reefcl  11605  efcj  11610  efaddlem  11611  efexp  11619  reeftlcl  11626  eftlub  11627  efsep  11628  effsumlt  11629  eflegeo  11638  retanclap  11659  demoivre  11709  demoivreALT  11710  eirraplem  11713  dvdsval3  11727  p1modz1  11730  iddvdsexp  11751  alzdvds  11788  addmodlteqALT  11793  nnehalf  11837  nno  11839  ndvdsadd  11864  divgcdnnr  11905  neggcd  11912  gcdabs  11917  bezoutlemmain  11927  bezoutlemaz  11932  bezoutlembz  11933  gcdmultiplez  11950  gcdzeq  11951  dvdssq  11960  algrf  11973  algcvg  11976  algcvga  11979  algfx  11980  eucalgf  11983  eucalgcvga  11986  neglcm  12003  lcmabs  12004  lcmdvds  12007  lcmgcdeq  12011  qredeq  12024  isprm3  12046  coprm  12072  prmrp  12073  isprm6  12075  prmdvdsexpb  12077  rpexp  12081  cncongrprm  12085  sqrt2irraplemnn  12107  phibndlem  12144  phiprmpw  12150  eulerthlemh  12159  eulerthlemth  12160  fermltl  12162  prmdivdiv  12165  modprm1div  12175  m1dvdsndvds  12176  coprimeprodsq  12185  pczpre  12225  pczcl  12226  pcexp  12237  pczdvds  12241  pczndvds  12243  pczndvds2  12245  pcdvdsb  12247  pcneg  12252  pcprmpw  12261  difsqpwdvds  12265  pcmptcl  12268  pcprod  12272  fldivp1  12274  infpnlem2  12286  1arithlem4  12292  ennnfonelemrn  12348  topnidg  12564  tgss3  12678  clsval  12711  clsss3  12730  neiss2  12742  resttop  12770  resttopon2  12778  lmconst  12816  cnima  12820  cnntri  12824  cncnp  12830  cnrest  12835  cndis  12841  lmss  12846  lmff  12849  lmtopcnp  12850  txcnp  12871  upxp  12872  uptx  12874  cnmpt11  12883  hmeoima  12910  hmeoopn  12911  hmeocld  12912  hmeontr  12913  hmeoimaf1o  12914  mettri2  12962  met0  12964  metres2  12981  blpnf  13000  xblss2ps  13004  xblss2  13005  blbas  13033  blres  13034  xmetec  13037  mopnss  13050  xmstri2  13070  mstri2  13071  xmstri  13072  mstri  13073  xmstri3  13074  mstri3  13075  msrtri  13076  mopni3  13084  unimopn  13086  comet  13099  bdxmet  13101  climcncf  13171  dedekindeulemuub  13195  dedekindicclemuub  13204  dvfgg  13257  dvidlemap  13260  dvfre  13274  reeff1olem  13292  reeff1o  13294  sinperlem  13329  abssinper  13367  reexplog  13392  relogexp  13393  cxpexpnn  13417  cxprec  13431  abscxp  13435  lgsdir  13536  lgsprme0  13543  lgsdinn0  13549  bj-inex  13749  bj-nn0suc  13806  bj-nn0sucALT  13820  trilpolemeq1  13879  trilpolemlt1  13880  trirec0  13883  nconstwlpolemgt0  13902