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  408  sylanr2  409  mpanr2  442  adantrl  482  adantrr  483  ancom2s  572  annimdc  950  ifpnst  1001  3adantr1  1187  3adantr2  1188  3adantr3  1189  syl3anr1  1330  syl3anr3  1332  dfbi3dc  1446  xordidc  1448  elabgt  2967  sbciegft  3082  csbtt  3159  csbnestgf  3200  copsex2t  4383  pofun  4455  onsucmin  4652  onsucelsucr  4653  onsucsssucr  4654  ordsucunielexmid  4676  ordsuc  4708  nlimsucg  4711  elnn  4751  xpsspw  4885  elxp4  5273  elxp5  5274  funimass2  5457  imain  5461  funimaexg  5463  f1ff1  5604  dff1o2  5642  resdif  5659  funbrfv  5736  fnbrfvb2  5742  fvelimab  5756  eqfnfv2  5801  fvimacnvi  5817  ffvresb  5865  fnressn  5895  fmptapd  5900  fnex  5931  rexima  5954  ralima  5955  f1elima  5973  fnotovb  6125  mpoeq12  6142  fovcdm  6226  fnovrn  6231  ofrfval  6305  ofvalg  6306  cofunexg  6332  cofunex2g  6333  mpoexxg  6440  mpoexg  6441  f1o2ndf1  6458  spc2ed  6463  funsssuppss  6492  smodm2  6560  tfrlem9  6584  tfrlemibxssdm  6592  tfr1onlembxssdm  6608  tfrcllembxssdm  6621  tfri3  6632  rdgtfr  6639  rdgruledefgg  6640  oav2  6730  oasuc  6731  omv2  6732  onasuc  6733  omsuc  6739  onmsuc  6740  nnaass  6752  nndi  6753  nndir  6757  nnaword  6778  ecelqsg  6856  iinerm  6875  ecovass  6912  ecoviass  6913  ecovdi  6914  ecovidi  6915  fvdiagfn  6969  ixpssmap2g  7003  domentr  7072  xpdom1g  7125  fopwdom  7130  ssenen  7146  phplem3  7149  phplem4  7150  php5dom  7158  ssfilem  7171  ssfilemd  7173  diffitest  7185  ctssdccl  7445  pm54.43  7530  pw1if  7578  addclpi  7688  addasspig  7691  mulasspig  7693  distrpig  7694  mulcanpig  7696  nnppipi  7704  enqdc1  7723  addassnqg  7743  ltbtwnnqq  7776  prarloclemarch  7779  prarloclemarch2  7780  enq0sym  7793  enq0ref  7794  addclnq0  7812  nqpnq0nq  7814  nnanq0  7819  distrnq0  7820  addassnq0lemcl  7822  addassnq0  7823  distnq0r  7824  prarloclemlt  7854  genpassl  7885  genpassu  7886  genpassg  7887  nqpru  7913  addcomprg  7939  mulcomprg  7941  distrlem1prl  7943  distrlem1pru  7944  1idprl  7951  1idpru  7952  recexprlemdisj  7991  recexprlem1ssl  7994  peano2nnnn  8214  ax1rid  8238  axcaucvglemcl  8256  le2tri3i  8428  add4  8481  cnegexlem1  8495  cnegexlem3  8497  cnegex  8498  subadd  8523  addsub  8531  addsubeq4  8535  negdi  8577  renegcl  8581  resubcl  8584  subdi  8706  mulneg2  8717  mul2neg  8719  submul2  8720  ltnegcon2  8786  lenegcon2  8789  lesub0  8801  cru  8924  recextlem1  8973  recexap  8975  div12ap  9018  divnegap  9030  letrp1  9172  dfinfre  9280  peano2nn  9299  nndivre  9323  nnsub  9326  nndivtr  9329  arch  9543  bndndx  9545  nn0addge1  9592  nn0addge2  9593  zaddcl  9667  zsubcl  9668  zltnle  9673  zrevaddcl  9678  nzadd  9680  zleltp1  9683  zltlem1  9685  zdiv  9717  peano2uz2  9736  uzind  9740  eluzp1l  9930  ublbneg  9996  qaddcl  10018  qsubcl  10021  qreccl  10025  qdivcl  10026  qrevaddcl  10027  irradd  10029  irrmul  10030  rerpdivcl  10068  nn0ledivnn  10151  xrre  10205  rexsub  10238  xaddass  10254  xnpcan  10257  xsubge0  10266  xposdif  10267  elioc2  10321  icoshft  10375  iccdil  10383  fzss2  10453  fzsuc2  10469  fzrev2  10475  elfzm11  10481  elfzp1b  10487  fzrevral  10495  fzshftral  10498  fzof  10534  fzoval  10538  fzon  10557  elfzoextl  10592  fzosubel  10595  zpnn0elfzo  10608  elfzom1b  10630  qltnle  10661  flqlt  10701  flqbi  10708  flqaddz  10715  fzofig  10852  seq3feq2  10896  ser3le  10957  expp1  10966  expm1t  10987  expeq0  10990  binom2sub  11073  bernneq  11081  expnlbnd  11085  zzlesq  11129  faccl  11156  facdiv  11159  bcpasc  11187  bccl  11188  ffz0hash  11259  fnfzo0hash  11261  hashfibclem  11265  hashf1lem2  11269  wrdlen1  11325  wrdred1  11330  ccatval21sw  11356  wrdl1exs1  11380  ccatws1cl  11383  ccatws1leng  11385  pfxmpt  11435  pfxfv  11439  pfxfvlsw  11450  ccatpfx  11456  pfx1  11458  swrdccatin1  11480  swrdccat  11490  pfxccatpfx1  11491  2shfti  11579  crim  11606  mulreap  11612  resub  11618  imsub  11626  ipcnval  11634  cjsub  11640  resqrexlemfp1  11758  resqrexlemgt0  11769  sqabsadd  11804  sqabssub  11805  abs2dif2  11856  cau3lem  11863  icodiamlt  11929  xrmaxaddlem  12009  clim  12030  clim2  12032  clim2c  12033  clim0c  12035  2clim  12050  climabs0  12056  climcn1  12057  climcn2  12058  climsqz  12084  climsqz2  12085  climub  12093  climserle  12094  fsum3cvg  12128  fisumss  12142  fsum3ser  12147  sumsplitdc  12182  fsump1i  12183  fsumlessfi  12210  telfsumo  12216  fsumparts  12220  iserabs  12225  binomlem  12233  isumsplit  12241  isum1p  12242  isumlessdc  12246  mertenslem2  12286  mertensabs  12287  prodfap0  12295  prodfrecap  12296  prodfdivap  12297  fproddccvg  12322  prodmodclem2  12327  fprodssdc  12340  fprodabs  12366  fprodeq0  12367  fprodeq0g  12388  ege2le3  12421  efsub  12431  efexp  12432  efsep  12441  sinsub  12490  cossub  12491  demoivre  12523  eirraplem  12527  moddvds  12549  0dvds  12561  iddvdsexp  12565  dvdssub  12588  dvdsle  12594  dvdsleabs  12595  dvdseq  12598  dvdsflip  12601  mulsucdiv2z  12635  divalgb  12675  divalg2  12676  ndvdsadd  12681  bitsp1  12701  gcdneg  12742  gcdabs2  12750  modgcd  12751  bezoutlemsup  12769  gcdmultiplez  12781  gcdeq  12783  dvdssq  12791  lcmcllem  12828  lcmneg  12835  lcmdvds  12840  qredeu  12858  cncongrcoprm  12867  isprm3  12879  prmrp  12906  divnumden  12957  phiprmpw  12983  crth  12985  hashgcdlem  12999  hashgcdeq  13001  modprminv  13011  modprminveq  13012  modprmn0modprm0  13018  coprimeprodsq2  13020  pcpre1  13054  pccl  13061  pcmul  13063  pcdiv  13064  pcqcl  13068  pcexp  13071  pcdvds  13077  pcndvds  13079  pcndvds2  13081  pcelnn  13083  pcgcd1  13090  pc2dvds  13092  pc11  13093  gzsubcl  13142  4sqlem3  13152  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemodife  13223  ballotfilemfrceq  13255  setsresg  13373  xpsfeq  13649  submcl  13769  grpinvnzcl  13860  mulgnnass  13943  nmzsubg  13996  nmznsg  13999  resghm2b  14048  ghmnsgpreima  14055  gzsumsnfd  14130  pwssnf1o  14194  iscrng2  14302  subrngpropd  14507  issubrg3  14538  subrgpropd  14544  islmodd  14612  lss1d  14703  lspsncl  14712  lspsnid  14727  df2idl2  14829  2idlcpbl  14844  qusrhm  14848  iunopn  15086  unopn  15089  eltg  15136  eltg2  15137  tgcl  15148  tgiun  15157  tgidm  15158  isopn3i  15219  isneip  15230  neipsm  15238  restbasg  15252  restopn2  15267  lmbrf  15299  cnclima  15307  lmss  15330  txbasval  15351  txlm  15363  psmetxrge0  15416  blininf  15508  blssps  15511  blss  15512  elmopn2  15533  bdmet  15586  metrest  15590  bl2ioo  15634  dvcjbr  15792  plyaddlem1  15831  plymullem1  15832  plyreres  15848  dvply1  15849  dvply2g  15850  efper  15891  sinperlem  15892  abssinper  15930  cxpexprp  15980  logcxp  15982  rpcxpcl  15988  rpcxproot  15999  rprelogbmulexp  16041  log2tlbndlog2  16065  lgsval2lem  16112  lgssq2  16143  lgsprme0  16144  ausgrusgrben  16392  wlkepvtx  16599  bj-inex  16916  peano5set  16949  findset  16954  bj-findis  16988  nninfsellemsuc  17029  nninfself  17030  cvgcmp2nlemabs  17055  iooref1o  17057  trilpolemeq1  17063  nconstwlpolemgt0  17088