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  1138  3adantl2  1139  3adantl3  1140  syl3anl1  1265  syl3anl3  1267  syl3anl  1268  stoic3  1408  eupick  2079  csbiebt  3044  csbnestgf  3057  reuss2  3361  mpteq12  4019  otexg  4160  opelopabt  4192  sonr  4247  sotr  4248  issod  4249  so2nr  4251  so3nr  4252  ordelss  4309  onelon  4314  elrnmpt1s  4797  iota2  5122  funeu  5156  imadif  5211  fnbr  5233  feu  5313  f1ss  5342  f1ssres  5345  f1resf1  5346  dffo2  5357  foco  5363  foun  5394  fun11iun  5396  ffoss  5407  funbrfv  5468  fvco3  5500  fvopab6  5525  funfvbrb  5541  elpreima  5547  ffvelrn  5561  ffvelrnda  5563  dffo4  5576  fmptco  5594  fsn2  5602  fvconst2g  5642  fex  5655  funfvima  5657  f1elima  5682  f1ocnvfv1  5686  f1ocnvfv2  5687  cocan2  5697  foeqcnvco  5699  isocnv  5720  isores2  5722  isoini  5727  isoselem  5729  f1oiso  5735  f1ofveu  5770  eloprabga  5866  grprinvlem  5973  suppssof1  6007  ofco  6008  offveqb  6009  fnexALT  6019  f1dmex  6022  ot1stg  6058  ot2ndg  6059  ot3rdgg  6060  eqopi  6078  2ndrn  6089  fo2ndf  6132  smores3  6198  smores2  6199  smoel  6205  smoiso  6207  tfrlem1  6213  tfrlemisucaccv  6230  tfrlemibxssdm  6232  tfrlemiubacc  6235  tfr1onlemsucaccv  6246  tfr1onlembfn  6249  tfr1onlemubacc  6251  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllemsucaccv  6259  tfrcllembfn  6262  tfrcllemubacc  6264  tfrcllemaccex  6266  tfrcllemres  6267  tfrcl  6269  frecrdg  6313  omv2  6369  nnasuc  6380  nnmsuc  6381  nnacom  6388  nnaass  6389  nnmass  6391  nntri1  6400  nndifsnid  6411  nnmordi  6420  swoer  6465  erth  6481  riinerm  6510  qliftlem  6515  ecovass  6546  ecoviass  6547  elmapssres  6575  fvixp  6605  f1domg  6660  endomtr  6692  xpsnen2g  6731  enen1  6742  enen2  6743  domen1  6744  domen2  6745  mapen  6748  mapxpen  6750  ssenen  6753  phplem1  6754  fidifsnid  6773  findcard  6790  findcard2  6791  findcard2s  6792  fieq0  6872  isotilem  6901  supisolem  6903  inflbti  6919  ordiso2  6928  djuex  6936  updjudhcoinlf  6973  updjudhcoinrg  6974  updjud  6975  ctssdccl  7004  enumctlemm  7007  finomni  7020  nnnninf  7031  pm54.43  7063  acfun  7080  ccfunen  7096  cc2lem  7098  cc3  7100  addclpi  7159  addasspig  7162  mulasspig  7164  addnidpig  7168  nnppipi  7175  ltanqi  7234  ltmnqi  7235  ltexnqq  7240  archnqq  7249  prarloclemarch2  7251  enq0sym  7264  enq0tr  7266  nqnq0pi  7270  nqnq0  7273  mulcanenq0ec  7277  addclnq0  7283  nqpnq0nq  7285  distrnq0  7291  addassnq0lemcl  7293  addassnq0  7294  prubl  7318  prarloclemlt  7325  genpdf  7340  genipv  7341  genpelvl  7344  genpelvu  7345  genpml  7349  genpmu  7350  genprndl  7353  genprndu  7354  genpassl  7356  genpassu  7357  genpassg  7358  addnqprl  7361  addnqpru  7362  addlocpr  7368  nqprm  7374  nqprl  7383  nqpru  7384  mulnqprl  7400  mulnqpru  7401  mullocprlem  7402  mullocpr  7403  addcomprg  7410  mulcomprg  7412  distrlem1prl  7414  distrlem1pru  7415  distrlem4prl  7416  distrlem4pru  7417  ltprordil  7421  1idprl  7422  1idpru  7423  ltpopr  7427  ltsopr  7428  ltaddpr  7429  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemfl  7441  ltexprlemrl  7442  ltexprlemfu  7443  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  prplnqu  7452  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  recexprlemss1l  7467  recexprlemss1u  7468  aptiprleml  7471  aptiprlemu  7472  cauappcvgprlemloc  7484  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemloc  7507  caucvgprlemladdrl  7510  caucvgprprlemml  7526  caucvgprprlemloc  7535  00sr  7601  map2psrprg  7637  suplocsrlempr  7639  suplocsrlem  7640  adddir  7781  axsuploc  7861  eqle  7879  le2tri3i  7896  mul4  7918  muladd11  7919  cnegexlem3  7963  addsub12  7999  2addsub  8000  addsubeq4  8001  subadd4  8030  negcon1  8038  negdi2  8044  negsubdi2  8045  neg2sub  8046  renegcl  8047  muladd  8170  subdir  8172  gt0ne0  8213  ltnegcon1  8249  lenegcon1  8252  eqord1  8269  eqord2  8270  recexre  8364  ltmul1  8378  recexap  8438  div12ap  8478  p1le  8631  ltmul2  8638  gt0div  8652  ge0div  8653  zlem1lt  9134  nnaddm1cl  9139  zdceq  9150  gtndiv  9170  prime  9174  msqznn  9175  btwnz  9194  uzss  9370  eluzadd  9378  nn0pzuz  9409  supinfneg  9417  infsupneg  9418  divfnzn  9440  qnegcl  9455  qreccl  9461  elpqb  9468  xaddass  9682  xleadd1a  9686  xlesubadd  9696  elico2  9750  iccss  9754  iccsupr  9779  elfz5  9829  fznn  9900  difelfznle  9943  fzoaddel  10000  qdceq  10055  qbtwnxr  10066  flqbi2  10095  adddivflid  10096  fldivnn0  10099  divfl0  10100  flqmulnn0  10103  fldivnn0le  10107  fldiv4p1lem1div2  10109  ceiqle  10117  flqdiv  10125  modqmulnn  10146  frecuzrdgtcl  10216  frecuzrdgsuc  10218  frecuzrdgdomlem  10221  frecuzrdgfunlem  10223  frecuzrdgsuctlem  10227  seq3caopr2  10286  iseqf1olemkle  10288  seq3f1olemp  10306  seq3id  10312  seq3z  10315  expap0  10354  mulexp  10363  mulexpzap  10364  expmul  10369  leexp1a  10379  expubnd  10381  zesq  10441  bernneq  10443  bernneq3  10445  facdiv  10516  facndiv  10517  faclbnd3  10521  faclbnd6  10522  bccmpl  10532  bcpasc  10544  bccl  10545  seq3coll  10617  shftlem  10620  ovshftex  10623  shftval4  10632  shftf  10634  shftcan2  10639  crim  10662  mulreap  10668  remul2  10677  immul2  10684  cjexp  10697  caucvgre  10785  r19.2uz  10797  sqrtsq2  10847  absnid  10877  absexp  10883  nn0abscl  10889  abslt  10892  lenegsq  10899  cau3lem  10918  minmax  11033  xrmaxadd  11062  clim  11082  climshftlemg  11103  climcn1  11109  climcn1lem  11120  clim2ser  11138  clim2ser2  11139  iserex  11140  isermulc2  11141  climub  11145  climcaucn  11152  serf0  11153  summodclem3  11181  summodclem2a  11182  summodclem2  11183  summodc  11184  fsum3  11188  fsumf1o  11191  fisumss  11193  isumss2  11194  fsumcl2lem  11199  fsumadd  11207  fsumsplit  11208  isummulc2  11227  fsum2d  11236  fsummulc2  11249  telfsumo  11267  fsumparts  11271  hash2iun1dif1  11281  bcxmas  11290  isumshft  11291  isumsplit  11292  expcnvap0  11303  geolim  11312  geolim2  11313  cvgratnnlemmn  11326  cvgratnnlemseq  11327  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  clim2divap  11341  prodmodclem3  11376  prodmodclem2a  11377  fprodseq  11384  efcllemp  11401  reefcl  11411  efcj  11416  efaddlem  11417  efexp  11425  reeftlcl  11432  eftlub  11433  efsep  11434  effsumlt  11435  eflegeo  11444  retanclap  11465  demoivre  11515  demoivreALT  11516  eirraplem  11519  dvdsval3  11533  iddvdsexp  11553  alzdvds  11588  addmodlteqALT  11593  nnehalf  11637  nno  11639  ndvdsadd  11664  divgcdnnr  11700  neggcd  11707  gcdabs  11712  bezoutlemmain  11722  bezoutlemaz  11727  bezoutlembz  11728  gcdmultiplez  11745  gcdzeq  11746  dvdssq  11755  algrf  11762  algcvg  11765  algcvga  11768  algfx  11769  eucalgf  11772  eucalgcvga  11775  neglcm  11792  lcmabs  11793  lcmdvds  11796  lcmgcdeq  11800  qredeq  11813  isprm3  11835  coprm  11858  prmrp  11859  isprm6  11861  prmdvdsexpb  11863  rpexp  11867  cncongrprm  11871  sqrt2irraplemnn  11893  phibndlem  11928  phiprmpw  11934  ennnfonelemrn  11968  topnidg  12172  tgss3  12286  clsval  12319  clsss3  12338  neiss2  12350  resttop  12378  resttopon2  12386  lmconst  12424  cnima  12428  cnntri  12432  cncnp  12438  cnrest  12443  cndis  12449  lmss  12454  lmff  12457  lmtopcnp  12458  txcnp  12479  upxp  12480  uptx  12482  cnmpt11  12491  hmeoima  12518  hmeoopn  12519  hmeocld  12520  hmeontr  12521  hmeoimaf1o  12522  mettri2  12570  met0  12572  metres2  12589  blpnf  12608  xblss2ps  12612  xblss2  12613  blbas  12641  blres  12642  xmetec  12645  mopnss  12658  xmstri2  12678  mstri2  12679  xmstri  12680  mstri  12681  xmstri3  12682  mstri3  12683  msrtri  12684  mopni3  12692  unimopn  12694  comet  12707  bdxmet  12709  climcncf  12779  dedekindeulemuub  12803  dedekindicclemuub  12812  dvfgg  12865  dvidlemap  12868  dvfre  12882  reeff1olem  12900  reeff1o  12902  sinperlem  12937  abssinper  12975  reexplog  13000  relogexp  13001  cxpexpnn  13025  cxprec  13039  abscxp  13043  bj-inex  13276  bj-nn0suc  13333  bj-nn0sucALT  13347  trilpolemeq1  13408  trilpolemlt1  13409  trirec0  13412