Theorem sylan2 286

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

Hypotheses

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

Assertion

Ref	Expression
sylan2	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan2.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 277	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylan2.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	syldan 282	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:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  404  sylanr2  405  mpanr2  438  adantrl  478  adantrr  479  ancom2s  568  annimdc  946  ifpnst  997  3adantr1  1183  3adantr2  1184  3adantr3  1185  syl3anr1  1326  syl3anr3  1328  dfbi3dc  1442  xordidc  1444  elabgt  2961  sbciegft  3076  csbtt  3153  csbnestgf  3194  copsex2t  4366  pofun  4438  onsucmin  4634  onsucelsucr  4635  onsucsssucr  4636  ordsucunielexmid  4658  ordsuc  4690  nlimsucg  4693  elnn  4733  xpsspw  4867  elxp4  5255  elxp5  5256  funimass2  5439  imain  5443  funimaexg  5445  f1ff1  5586  dff1o2  5624  resdif  5641  funbrfv  5718  fnbrfvb2  5724  fvelimab  5738  eqfnfv2  5781  fvimacnvi  5797  ffvresb  5845  fnressn  5875  fmptapd  5880  fnex  5911  rexima  5933  ralima  5934  f1elima  5952  fnotovb  6104  mpoeq12  6121  fovcdm  6205  fnovrn  6210  ofrfval  6284  ofvalg  6285  cofunexg  6311  cofunex2g  6312  mpoexxg  6419  mpoexg  6420  f1o2ndf1  6437  spc2ed  6442  funsssuppss  6471  smodm2  6539  tfrlem9  6563  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  tfri3  6611  rdgtfr  6618  rdgruledefgg  6619  oav2  6709  oasuc  6710  omv2  6711  onasuc  6712  omsuc  6718  onmsuc  6719  nnaass  6731  nndi  6732  nndir  6736  nnaword  6757  ecelqsg  6835  iinerm  6854  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  fvdiagfn  6941  ixpssmap2g  6975  domentr  7044  xpdom1g  7097  fopwdom  7102  ssenen  7118  phplem3  7121  phplem4  7122  php5dom  7130  ssfilem  7143  ssfilemd  7145  diffitest  7157  ctssdccl  7415  pm54.43  7500  pw1if  7548  addclpi  7658  addasspig  7661  mulasspig  7663  distrpig  7664  mulcanpig  7666  nnppipi  7674  enqdc1  7693  addassnqg  7713  ltbtwnnqq  7746  prarloclemarch  7749  prarloclemarch2  7750  enq0sym  7763  enq0ref  7764  addclnq0  7782  nqpnq0nq  7784  nnanq0  7789  distrnq0  7790  addassnq0lemcl  7792  addassnq0  7793  distnq0r  7794  prarloclemlt  7824  genpassl  7855  genpassu  7856  genpassg  7857  nqpru  7883  addcomprg  7909  mulcomprg  7911  distrlem1prl  7913  distrlem1pru  7914  1idprl  7921  1idpru  7922  recexprlemdisj  7961  recexprlem1ssl  7964  peano2nnnn  8184  ax1rid  8208  axcaucvglemcl  8226  le2tri3i  8398  add4  8451  cnegexlem1  8465  cnegexlem3  8467  cnegex  8468  subadd  8493  addsub  8501  addsubeq4  8505  negdi  8547  renegcl  8551  resubcl  8554  subdi  8676  mulneg2  8687  mul2neg  8689  submul2  8690  ltnegcon2  8756  lenegcon2  8759  lesub0  8771  cru  8894  recextlem1  8943  recexap  8945  div12ap  8988  divnegap  9000  letrp1  9142  dfinfre  9250  peano2nn  9269  nndivre  9293  nnsub  9296  nndivtr  9299  arch  9513  bndndx  9515  nn0addge1  9562  nn0addge2  9563  zaddcl  9637  zsubcl  9638  zltnle  9643  zrevaddcl  9648  nzadd  9650  zleltp1  9653  zltlem1  9655  zdiv  9687  peano2uz2  9706  uzind  9710  eluzp1l  9900  ublbneg  9966  qaddcl  9988  qsubcl  9991  qreccl  9995  qdivcl  9996  qrevaddcl  9997  irradd  9999  irrmul  10000  rerpdivcl  10038  nn0ledivnn  10121  xrre  10175  rexsub  10208  xaddass  10224  xnpcan  10227  xsubge0  10236  xposdif  10237  elioc2  10291  icoshft  10345  iccdil  10353  fzss2  10422  fzsuc2  10438  fzrev2  10444  elfzm11  10450  elfzp1b  10456  fzrevral  10464  fzshftral  10467  fzof  10503  fzoval  10507  fzon  10526  elfzoextl  10561  fzosubel  10564  zpnn0elfzo  10577  elfzom1b  10599  qltnle  10630  flqlt  10670  flqbi  10677  flqaddz  10684  fzofig  10821  seq3feq2  10865  ser3le  10926  expp1  10935  expm1t  10956  expeq0  10959  binom2sub  11042  bernneq  11050  expnlbnd  11054  zzlesq  11098  faccl  11125  facdiv  11128  bcpasc  11156  bccl  11157  ffz0hash  11228  fnfzo0hash  11230  hashfibclem  11234  wrdlen1  11290  wrdred1  11295  ccatval21sw  11321  wrdl1exs1  11345  ccatws1cl  11348  ccatws1leng  11350  pfxmpt  11400  pfxfv  11404  pfxfvlsw  11415  ccatpfx  11421  pfx1  11423  swrdccatin1  11445  swrdccat  11455  pfxccatpfx1  11456  2shfti  11544  crim  11571  mulreap  11577  resub  11583  imsub  11591  ipcnval  11599  cjsub  11605  resqrexlemfp1  11723  resqrexlemgt0  11734  sqabsadd  11769  sqabssub  11770  abs2dif2  11821  cau3lem  11828  icodiamlt  11894  xrmaxaddlem  11974  clim  11995  clim2  11997  clim2c  11998  clim0c  12000  2clim  12015  climabs0  12021  climcn1  12022  climcn2  12023  climsqz  12049  climsqz2  12050  climub  12058  climserle  12059  fsum3cvg  12093  fisumss  12107  fsum3ser  12112  sumsplitdc  12147  fsump1i  12148  fsumlessfi  12175  telfsumo  12181  fsumparts  12185  iserabs  12190  binomlem  12198  isumsplit  12206  isum1p  12207  isumlessdc  12211  mertenslem2  12251  mertensabs  12252  prodfap0  12260  prodfrecap  12261  prodfdivap  12262  fproddccvg  12287  prodmodclem2  12292  fprodssdc  12305  fprodabs  12331  fprodeq0  12332  fprodeq0g  12353  ege2le3  12386  efsub  12396  efexp  12397  efsep  12406  sinsub  12455  cossub  12456  demoivre  12488  eirraplem  12492  moddvds  12514  0dvds  12526  iddvdsexp  12530  dvdssub  12553  dvdsle  12559  dvdsleabs  12560  dvdseq  12563  dvdsflip  12566  mulsucdiv2z  12600  divalgb  12640  divalg2  12641  ndvdsadd  12646  bitsp1  12666  gcdneg  12707  gcdabs2  12715  modgcd  12716  bezoutlemsup  12734  gcdmultiplez  12746  gcdeq  12748  dvdssq  12756  lcmcllem  12793  lcmneg  12800  lcmdvds  12805  qredeu  12823  cncongrcoprm  12832  isprm3  12844  prmrp  12871  divnumden  12922  phiprmpw  12948  crth  12950  hashgcdlem  12964  hashgcdeq  12966  modprminv  12976  modprminveq  12977  modprmn0modprm0  12983  coprimeprodsq2  12985  pcpre1  13019  pccl  13026  pcmul  13028  pcdiv  13029  pcqcl  13033  pcexp  13036  pcdvds  13042  pcndvds  13044  pcndvds2  13046  pcelnn  13048  pcgcd1  13055  pc2dvds  13057  pc11  13058  gzsubcl  13107  4sqlem3  13117  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemodife  13188  ballotfilemfrceq  13220  setsresg  13338  xpsfeq  13613  submcl  13738  grpinvnzcl  13831  mulgnnass  13914  nmzsubg  13967  nmznsg  13970  resghm2b  14019  ghmnsgpreima  14026  gsumfzsnfd  14102  pwssnf1o  14157  iscrng2  14262  subrngpropd  14466  issubrg3  14497  subrgpropd  14503  islmodd  14571  lss1d  14661  lspsncl  14670  lspsnid  14685  df2idl2  14787  2idlcpbl  14802  qusrhm  14806  gsumfzfsumlemm  14865  iunopn  14997  unopn  15000  eltg  15047  eltg2  15048  tgcl  15059  tgiun  15068  tgidm  15069  isopn3i  15130  isneip  15141  neipsm  15149  restbasg  15163  restopn2  15178  lmbrf  15210  cnclima  15218  lmss  15241  txbasval  15262  txlm  15274  psmetxrge0  15327  blininf  15419  blssps  15422  blss  15423  elmopn2  15444  bdmet  15497  metrest  15501  bl2ioo  15545  dvcjbr  15703  plyaddlem1  15742  plymullem1  15743  plyreres  15759  dvply1  15760  dvply2g  15761  efper  15802  sinperlem  15803  abssinper  15841  cxpexprp  15890  logcxp  15892  rpcxpcl  15898  rpcxproot  15909  rprelogbmulexp  15951  lgsval2lem  16013  lgssq2  16044  lgsprme0  16045  ausgrusgrben  16293  wlkepvtx  16500  bj-inex  16817  peano5set  16850  findset  16855  bj-findis  16889  nninfsellemsuc  16930  nninfself  16931  cvgcmp2nlemabs  16956  iooref1o  16958  trilpolemeq1  16964  nconstwlpolemgt0  16989