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  2948  sbciegft  3063  csbtt  3140  csbnestgf  3181  copsex2t  4343  pofun  4415  onsucmin  4611  onsucelsucr  4612  onsucsssucr  4613  ordsucunielexmid  4635  ordsuc  4667  nlimsucg  4670  elnn  4710  xpsspw  4844  elxp4  5231  elxp5  5232  funimass2  5415  imain  5419  funimaexg  5421  f1ff1  5559  dff1o2  5597  resdif  5614  funbrfv  5691  fnbrfvb2  5697  fvelimab  5711  eqfnfv2  5754  fvimacnvi  5770  ffvresb  5818  fnressn  5848  fmptapd  5853  fnex  5884  rexima  5905  ralima  5906  f1elima  5924  fnotovb  6074  mpoeq12  6091  fovcdm  6175  fnovrn  6180  ofrfval  6253  ofvalg  6254  cofunexg  6280  cofunex2g  6281  mpoexxg  6384  mpoexg  6385  f1o2ndf1  6402  spc2ed  6407  funsssuppss  6436  smodm2  6504  tfrlem9  6528  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  tfri3  6576  rdgtfr  6583  rdgruledefgg  6584  oav2  6674  oasuc  6675  omv2  6676  onasuc  6677  omsuc  6683  onmsuc  6684  nnaass  6696  nndi  6697  nndir  6701  nnaword  6722  ecelqsg  6800  iinerm  6819  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  fvdiagfn  6905  ixpssmap2g  6939  domentr  7008  xpdom1g  7060  fopwdom  7065  ssenen  7080  phplem3  7083  phplem4  7084  php5dom  7092  ssfilem  7105  ssfilemd  7107  diffitest  7119  ctssdccl  7353  pm54.43  7438  pw1if  7486  addclpi  7590  addasspig  7593  mulasspig  7595  distrpig  7596  mulcanpig  7598  nnppipi  7606  enqdc1  7625  addassnqg  7645  ltbtwnnqq  7678  prarloclemarch  7681  prarloclemarch2  7682  enq0sym  7695  enq0ref  7696  addclnq0  7714  nqpnq0nq  7716  nnanq0  7721  distrnq0  7722  addassnq0lemcl  7724  addassnq0  7725  distnq0r  7726  prarloclemlt  7756  genpassl  7787  genpassu  7788  genpassg  7789  nqpru  7815  addcomprg  7841  mulcomprg  7843  distrlem1prl  7845  distrlem1pru  7846  1idprl  7853  1idpru  7854  recexprlemdisj  7893  recexprlem1ssl  7896  peano2nnnn  8116  ax1rid  8140  axcaucvglemcl  8158  le2tri3i  8331  add4  8383  cnegexlem1  8397  cnegexlem3  8399  cnegex  8400  subadd  8425  addsub  8433  addsubeq4  8437  negdi  8479  renegcl  8483  resubcl  8486  subdi  8607  mulneg2  8618  mul2neg  8620  submul2  8621  ltnegcon2  8687  lenegcon2  8690  lesub0  8702  cru  8825  recextlem1  8874  recexap  8876  div12ap  8917  divnegap  8929  letrp1  9071  dfinfre  9179  peano2nn  9198  nndivre  9222  nnsub  9225  nndivtr  9228  arch  9442  bndndx  9444  nn0addge1  9491  nn0addge2  9492  zaddcl  9562  zsubcl  9563  zltnle  9568  zrevaddcl  9573  nzadd  9575  zleltp1  9578  zltlem1  9580  zdiv  9611  peano2uz2  9630  uzind  9634  eluzp1l  9824  ublbneg  9890  qaddcl  9912  qsubcl  9915  qreccl  9919  qdivcl  9920  qrevaddcl  9921  irradd  9923  irrmul  9924  rerpdivcl  9962  nn0ledivnn  10045  xrre  10098  rexsub  10131  xaddass  10147  xnpcan  10150  xsubge0  10159  xposdif  10160  elioc2  10214  icoshft  10268  iccdil  10276  fzss2  10342  fzsuc2  10357  fzrev2  10363  elfzm11  10369  elfzp1b  10375  fzrevral  10383  fzshftral  10386  fzof  10422  fzoval  10426  fzon  10445  elfzoextl  10480  fzosubel  10483  zpnn0elfzo  10496  elfzom1b  10518  qltnle  10547  flqlt  10587  flqbi  10594  flqaddz  10601  fzofig  10738  seq3feq2  10782  ser3le  10843  expp1  10852  expm1t  10873  expeq0  10876  binom2sub  10959  bernneq  10966  expnlbnd  10970  zzlesq  11014  faccl  11041  facdiv  11044  bcpasc  11072  bccl  11073  ffz0hash  11141  fnfzo0hash  11143  wrdlen1  11198  wrdred1  11203  ccatval21sw  11229  wrdl1exs1  11253  ccatws1cl  11256  ccatws1leng  11258  pfxmpt  11308  pfxfv  11312  pfxfvlsw  11323  ccatpfx  11329  pfx1  11331  swrdccatin1  11353  swrdccat  11363  pfxccatpfx1  11364  2shfti  11452  crim  11479  mulreap  11485  resub  11491  imsub  11499  ipcnval  11507  cjsub  11513  resqrexlemfp1  11630  resqrexlemgt0  11641  sqabsadd  11676  sqabssub  11677  abs2dif2  11728  cau3lem  11735  icodiamlt  11801  xrmaxaddlem  11881  clim  11902  clim2  11904  clim2c  11905  clim0c  11907  2clim  11922  climabs0  11928  climcn1  11929  climcn2  11930  climsqz  11956  climsqz2  11957  climub  11965  climserle  11966  fsum3cvg  12000  fisumss  12014  fsum3ser  12019  sumsplitdc  12054  fsump1i  12055  fsumlessfi  12082  telfsumo  12088  fsumparts  12092  iserabs  12097  binomlem  12105  isumsplit  12113  isum1p  12114  isumlessdc  12118  mertenslem2  12158  mertensabs  12159  prodfap0  12167  prodfrecap  12168  prodfdivap  12169  fproddccvg  12194  prodmodclem2  12199  fprodssdc  12212  fprodabs  12238  fprodeq0  12239  fprodeq0g  12260  ege2le3  12293  efsub  12303  efexp  12304  efsep  12313  sinsub  12362  cossub  12363  demoivre  12395  eirraplem  12399  moddvds  12421  0dvds  12433  iddvdsexp  12437  dvdssub  12460  dvdsle  12466  dvdsleabs  12467  dvdseq  12470  dvdsflip  12473  mulsucdiv2z  12507  divalgb  12547  divalg2  12548  ndvdsadd  12553  bitsp1  12573  gcdneg  12614  gcdabs2  12622  modgcd  12623  bezoutlemsup  12641  gcdmultiplez  12653  gcdeq  12655  dvdssq  12663  lcmcllem  12700  lcmneg  12707  lcmdvds  12712  qredeu  12730  cncongrcoprm  12739  isprm3  12751  prmrp  12778  divnumden  12829  phiprmpw  12855  crth  12857  hashgcdlem  12871  hashgcdeq  12873  modprminv  12883  modprminveq  12884  modprmn0modprm0  12890  coprimeprodsq2  12892  pcpre1  12926  pccl  12933  pcmul  12935  pcdiv  12936  pcqcl  12940  pcexp  12943  pcdvds  12949  pcndvds  12951  pcndvds2  12953  pcelnn  12955  pcgcd1  12962  pc2dvds  12964  pc11  12965  gzsubcl  13014  4sqlem3  13024  setsresg  13181  pwssnf1o  13442  xpsfeq  13489  submcl  13623  grpinvnzcl  13716  mulgnnass  13805  nmzsubg  13858  nmznsg  13861  resghm2b  13910  ghmnsgpreima  13917  gsumfzsnfd  13993  iscrng2  14090  subrngpropd  14292  issubrg3  14323  subrgpropd  14329  islmodd  14369  lss1d  14459  lspsncl  14468  lspsnid  14483  df2idl2  14585  2idlcpbl  14600  qusrhm  14604  gsumfzfsumlemm  14663  iunopn  14793  unopn  14796  eltg  14843  eltg2  14844  tgcl  14855  tgiun  14864  tgidm  14865  isopn3i  14926  isneip  14937  neipsm  14945  restbasg  14959  restopn2  14974  lmbrf  15006  cnclima  15014  lmss  15037  txbasval  15058  txlm  15070  psmetxrge0  15123  blininf  15215  blssps  15218  blss  15219  elmopn2  15240  bdmet  15293  metrest  15297  bl2ioo  15341  dvcjbr  15499  plyaddlem1  15538  plymullem1  15539  plyreres  15555  dvply1  15556  dvply2g  15557  efper  15598  sinperlem  15599  abssinper  15637  cxpexprp  15686  logcxp  15688  rpcxpcl  15694  rpcxproot  15705  rprelogbmulexp  15747  lgsval2lem  15809  lgssq2  15840  lgsprme0  15841  ausgrusgrben  16089  wlkepvtx  16296  bj-inex  16603  peano5set  16636  findset  16641  bj-findis  16675  nninfsellemsuc  16718  nninfself  16719  cvgcmp2nlemabs  16744  iooref1o  16746  trilpolemeq1  16752  nconstwlpolemgt0  16777