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  945  ifpnst  996  3adantr1  1182  3adantr2  1183  3adantr3  1184  syl3anr1  1325  syl3anr3  1327  dfbi3dc  1441  xordidc  1443  elabgt  2947  sbciegft  3062  csbtt  3139  csbnestgf  3180  copsex2t  4337  pofun  4409  onsucmin  4605  onsucelsucr  4606  onsucsssucr  4607  ordsucunielexmid  4629  ordsuc  4661  nlimsucg  4664  elnn  4704  xpsspw  4838  elxp4  5224  elxp5  5225  funimass2  5408  imain  5412  funimaexg  5414  f1ff1  5550  dff1o2  5588  resdif  5605  funbrfv  5682  fnbrfvb2  5688  fvelimab  5702  eqfnfv2  5745  fvimacnvi  5761  ffvresb  5810  fnressn  5840  fmptapd  5845  fnex  5876  rexima  5895  ralima  5896  f1elima  5914  fnotovb  6064  mpoeq12  6081  fovcdm  6165  fnovrn  6170  ofrfval  6244  ofvalg  6245  cofunexg  6271  cofunex2g  6272  mpoexxg  6375  mpoexg  6376  f1o2ndf1  6393  spc2ed  6398  smodm2  6461  tfrlem9  6485  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  tfri3  6533  rdgtfr  6540  rdgruledefgg  6541  oav2  6631  oasuc  6632  omv2  6633  onasuc  6634  omsuc  6640  onmsuc  6641  nnaass  6653  nndi  6654  nndir  6658  nnaword  6679  ecelqsg  6757  iinerm  6776  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  fvdiagfn  6862  ixpssmap2g  6896  domentr  6965  xpdom1g  7017  fopwdom  7022  ssenen  7037  phplem3  7040  phplem4  7041  php5dom  7049  ssfilem  7062  ssfilemd  7064  diffitest  7076  ctssdccl  7310  pm54.43  7395  pw1if  7443  addclpi  7547  addasspig  7550  mulasspig  7552  distrpig  7553  mulcanpig  7555  nnppipi  7563  enqdc1  7582  addassnqg  7602  ltbtwnnqq  7635  prarloclemarch  7638  prarloclemarch2  7639  enq0sym  7652  enq0ref  7653  addclnq0  7671  nqpnq0nq  7673  nnanq0  7678  distrnq0  7679  addassnq0lemcl  7681  addassnq0  7682  distnq0r  7683  prarloclemlt  7713  genpassl  7744  genpassu  7745  genpassg  7746  nqpru  7772  addcomprg  7798  mulcomprg  7800  distrlem1prl  7802  distrlem1pru  7803  1idprl  7810  1idpru  7811  recexprlemdisj  7850  recexprlem1ssl  7853  peano2nnnn  8073  ax1rid  8097  axcaucvglemcl  8115  le2tri3i  8288  add4  8340  cnegexlem1  8354  cnegexlem3  8356  cnegex  8357  subadd  8382  addsub  8390  addsubeq4  8394  negdi  8436  renegcl  8440  resubcl  8443  subdi  8564  mulneg2  8575  mul2neg  8577  submul2  8578  ltnegcon2  8644  lenegcon2  8647  lesub0  8659  cru  8782  recextlem1  8831  recexap  8833  div12ap  8874  divnegap  8886  letrp1  9028  dfinfre  9136  peano2nn  9155  nndivre  9179  nnsub  9182  nndivtr  9185  arch  9399  bndndx  9401  nn0addge1  9448  nn0addge2  9449  zaddcl  9519  zsubcl  9520  zltnle  9525  zrevaddcl  9530  nzadd  9532  zleltp1  9535  zltlem1  9537  zdiv  9568  peano2uz2  9587  uzind  9591  eluzp1l  9781  ublbneg  9847  qaddcl  9869  qsubcl  9872  qreccl  9876  qdivcl  9877  qrevaddcl  9878  irradd  9880  irrmul  9881  rerpdivcl  9919  nn0ledivnn  10002  xrre  10055  rexsub  10088  xaddass  10104  xnpcan  10107  xsubge0  10116  xposdif  10117  elioc2  10171  icoshft  10225  iccdil  10233  fzss2  10299  fzsuc2  10314  fzrev2  10320  elfzm11  10326  elfzp1b  10332  fzrevral  10340  fzshftral  10343  fzof  10379  fzoval  10383  fzon  10402  elfzoextl  10437  fzosubel  10440  zpnn0elfzo  10453  elfzom1b  10475  qltnle  10504  flqlt  10544  flqbi  10551  flqaddz  10558  fzofig  10695  seq3feq2  10739  ser3le  10800  expp1  10809  expm1t  10830  expeq0  10833  binom2sub  10916  bernneq  10923  expnlbnd  10927  zzlesq  10971  faccl  10998  facdiv  11001  bcpasc  11029  bccl  11030  ffz0hash  11098  fnfzo0hash  11100  wrdlen1  11155  wrdred1  11160  ccatval21sw  11186  wrdl1exs1  11210  ccatws1cl  11213  ccatws1leng  11215  pfxmpt  11265  pfxfv  11269  pfxfvlsw  11280  ccatpfx  11286  pfx1  11288  swrdccatin1  11310  swrdccat  11320  pfxccatpfx1  11321  2shfti  11396  crim  11423  mulreap  11429  resub  11435  imsub  11443  ipcnval  11451  cjsub  11457  resqrexlemfp1  11574  resqrexlemgt0  11585  sqabsadd  11620  sqabssub  11621  abs2dif2  11672  cau3lem  11679  icodiamlt  11745  xrmaxaddlem  11825  clim  11846  clim2  11848  clim2c  11849  clim0c  11851  2clim  11866  climabs0  11872  climcn1  11873  climcn2  11874  climsqz  11900  climsqz2  11901  climub  11909  climserle  11910  fsum3cvg  11944  fisumss  11958  fsum3ser  11963  sumsplitdc  11998  fsump1i  11999  fsumlessfi  12026  telfsumo  12032  fsumparts  12036  iserabs  12041  binomlem  12049  isumsplit  12057  isum1p  12058  isumlessdc  12062  mertenslem2  12102  mertensabs  12103  prodfap0  12111  prodfrecap  12112  prodfdivap  12113  fproddccvg  12138  prodmodclem2  12143  fprodssdc  12156  fprodabs  12182  fprodeq0  12183  fprodeq0g  12204  ege2le3  12237  efsub  12247  efexp  12248  efsep  12257  sinsub  12306  cossub  12307  demoivre  12339  eirraplem  12343  moddvds  12365  0dvds  12377  iddvdsexp  12381  dvdssub  12404  dvdsle  12410  dvdsleabs  12411  dvdseq  12414  dvdsflip  12417  mulsucdiv2z  12451  divalgb  12491  divalg2  12492  ndvdsadd  12497  bitsp1  12517  gcdneg  12558  gcdabs2  12566  modgcd  12567  bezoutlemsup  12585  gcdmultiplez  12597  gcdeq  12599  dvdssq  12607  lcmcllem  12644  lcmneg  12651  lcmdvds  12656  qredeu  12674  cncongrcoprm  12683  isprm3  12695  prmrp  12722  divnumden  12773  phiprmpw  12799  crth  12801  hashgcdlem  12815  hashgcdeq  12817  modprminv  12827  modprminveq  12828  modprmn0modprm0  12834  coprimeprodsq2  12836  pcpre1  12870  pccl  12877  pcmul  12879  pcdiv  12880  pcqcl  12884  pcexp  12887  pcdvds  12893  pcndvds  12895  pcndvds2  12897  pcelnn  12899  pcgcd1  12906  pc2dvds  12908  pc11  12909  gzsubcl  12958  4sqlem3  12968  setsresg  13125  pwssnf1o  13386  xpsfeq  13433  submcl  13567  grpinvnzcl  13660  mulgnnass  13749  nmzsubg  13802  nmznsg  13805  resghm2b  13854  ghmnsgpreima  13861  gsumfzsnfd  13937  iscrng2  14034  subrngpropd  14236  issubrg3  14267  subrgpropd  14273  islmodd  14313  lss1d  14403  lspsncl  14412  lspsnid  14427  df2idl2  14529  2idlcpbl  14544  qusrhm  14548  gsumfzfsumlemm  14607  iunopn  14732  unopn  14735  eltg  14782  eltg2  14783  tgcl  14794  tgiun  14803  tgidm  14804  isopn3i  14865  isneip  14876  neipsm  14884  restbasg  14898  restopn2  14913  lmbrf  14945  cnclima  14953  lmss  14976  txbasval  14997  txlm  15009  psmetxrge0  15062  blininf  15154  blssps  15157  blss  15158  elmopn2  15179  bdmet  15232  metrest  15236  bl2ioo  15280  dvcjbr  15438  plyaddlem1  15477  plymullem1  15478  plyreres  15494  dvply1  15495  dvply2g  15496  efper  15537  sinperlem  15538  abssinper  15576  cxpexprp  15625  logcxp  15627  rpcxpcl  15633  rpcxproot  15644  rprelogbmulexp  15686  lgsval2lem  15745  lgssq2  15776  lgsprme0  15777  ausgrusgrben  16025  wlkepvtx  16232  bj-inex  16528  peano5set  16561  findset  16566  bj-findis  16600  nninfsellemsuc  16640  nninfself  16641  cvgcmp2nlemabs  16662  iooref1o  16664  trilpolemeq1  16670  nconstwlpolemgt0  16694