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  566  annimdc  943  ifpnst  994  3adantr1  1180  3adantr2  1181  3adantr3  1182  syl3anr1  1323  syl3anr3  1325  dfbi3dc  1439  xordidc  1441  elabgt  2944  sbciegft  3059  csbtt  3136  csbnestgf  3177  copsex2t  4332  pofun  4404  onsucmin  4600  onsucelsucr  4601  onsucsssucr  4602  ordsucunielexmid  4624  ordsuc  4656  nlimsucg  4659  elnn  4699  xpsspw  4833  elxp4  5219  elxp5  5220  funimass2  5402  imain  5406  funimaexg  5408  f1ff1  5544  dff1o2  5582  resdif  5599  funbrfv  5675  fnbrfvb2  5681  fvelimab  5695  eqfnfv2  5738  fvimacnvi  5754  ffvresb  5803  fnressn  5832  fmptapd  5837  fnex  5868  rexima  5887  ralima  5888  f1elima  5906  fnotovb  6056  mpoeq12  6073  fovcdm  6157  fnovrn  6162  ofrfval  6236  ofvalg  6237  cofunexg  6263  cofunex2g  6264  mpoexxg  6367  mpoexg  6368  f1o2ndf1  6385  spc2ed  6390  smodm2  6452  tfrlem9  6476  tfrlemibxssdm  6484  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  tfri3  6524  rdgtfr  6531  rdgruledefgg  6532  oav2  6622  oasuc  6623  omv2  6624  onasuc  6625  omsuc  6631  onmsuc  6632  nnaass  6644  nndi  6645  nndir  6649  nnaword  6670  ecelqsg  6748  iinerm  6767  ecovass  6804  ecoviass  6805  ecovdi  6806  ecovidi  6807  fvdiagfn  6853  ixpssmap2g  6887  domentr  6956  xpdom1g  7005  fopwdom  7010  ssenen  7025  phplem3  7028  phplem4  7029  php5dom  7037  ssfilem  7050  diffitest  7062  ctssdccl  7294  pm54.43  7379  pw1if  7426  addclpi  7530  addasspig  7533  mulasspig  7535  distrpig  7536  mulcanpig  7538  nnppipi  7546  enqdc1  7565  addassnqg  7585  ltbtwnnqq  7618  prarloclemarch  7621  prarloclemarch2  7622  enq0sym  7635  enq0ref  7636  addclnq0  7654  nqpnq0nq  7656  nnanq0  7661  distrnq0  7662  addassnq0lemcl  7664  addassnq0  7665  distnq0r  7666  prarloclemlt  7696  genpassl  7727  genpassu  7728  genpassg  7729  nqpru  7755  addcomprg  7781  mulcomprg  7783  distrlem1prl  7785  distrlem1pru  7786  1idprl  7793  1idpru  7794  recexprlemdisj  7833  recexprlem1ssl  7836  peano2nnnn  8056  ax1rid  8080  axcaucvglemcl  8098  le2tri3i  8271  add4  8323  cnegexlem1  8337  cnegexlem3  8339  cnegex  8340  subadd  8365  addsub  8373  addsubeq4  8377  negdi  8419  renegcl  8423  resubcl  8426  subdi  8547  mulneg2  8558  mul2neg  8560  submul2  8561  ltnegcon2  8627  lenegcon2  8630  lesub0  8642  cru  8765  recextlem1  8814  recexap  8816  div12ap  8857  divnegap  8869  letrp1  9011  dfinfre  9119  peano2nn  9138  nndivre  9162  nnsub  9165  nndivtr  9168  arch  9382  bndndx  9384  nn0addge1  9431  nn0addge2  9432  zaddcl  9502  zsubcl  9503  zltnle  9508  zrevaddcl  9513  nzadd  9515  zleltp1  9518  zltlem1  9520  zdiv  9551  peano2uz2  9570  uzind  9574  eluzp1l  9764  ublbneg  9825  qaddcl  9847  qsubcl  9850  qreccl  9854  qdivcl  9855  qrevaddcl  9856  irradd  9858  irrmul  9859  rerpdivcl  9897  nn0ledivnn  9980  xrre  10033  rexsub  10066  xaddass  10082  xnpcan  10085  xsubge0  10094  xposdif  10095  elioc2  10149  icoshft  10203  iccdil  10211  fzss2  10277  fzsuc2  10292  fzrev2  10298  elfzm11  10304  elfzp1b  10310  fzrevral  10318  fzshftral  10321  fzof  10357  fzoval  10361  fzon  10380  elfzoextl  10414  fzosubel  10417  zpnn0elfzo  10430  elfzom1b  10452  qltnle  10480  flqlt  10520  flqbi  10527  flqaddz  10534  fzofig  10671  seq3feq2  10715  ser3le  10776  expp1  10785  expm1t  10806  expeq0  10809  binom2sub  10892  bernneq  10899  expnlbnd  10903  zzlesq  10947  faccl  10974  facdiv  10977  bcpasc  11005  bccl  11006  ffz0hash  11073  fnfzo0hash  11075  wrdlen1  11127  wrdred1  11132  ccatval21sw  11158  wrdl1exs1  11182  ccatws1cl  11185  ccatws1leng  11187  pfxmpt  11233  pfxfv  11237  pfxfvlsw  11248  ccatpfx  11254  pfx1  11256  swrdccatin1  11278  swrdccat  11288  pfxccatpfx1  11289  2shfti  11363  crim  11390  mulreap  11396  resub  11402  imsub  11410  ipcnval  11418  cjsub  11424  resqrexlemfp1  11541  resqrexlemgt0  11552  sqabsadd  11587  sqabssub  11588  abs2dif2  11639  cau3lem  11646  icodiamlt  11712  xrmaxaddlem  11792  clim  11813  clim2  11815  clim2c  11816  clim0c  11818  2clim  11833  climabs0  11839  climcn1  11840  climcn2  11841  climsqz  11867  climsqz2  11868  climub  11876  climserle  11877  fsum3cvg  11910  fisumss  11924  fsum3ser  11929  sumsplitdc  11964  fsump1i  11965  fsumlessfi  11992  telfsumo  11998  fsumparts  12002  iserabs  12007  binomlem  12015  isumsplit  12023  isum1p  12024  isumlessdc  12028  mertenslem2  12068  mertensabs  12069  prodfap0  12077  prodfrecap  12078  prodfdivap  12079  fproddccvg  12104  prodmodclem2  12109  fprodssdc  12122  fprodabs  12148  fprodeq0  12149  fprodeq0g  12170  ege2le3  12203  efsub  12213  efexp  12214  efsep  12223  sinsub  12272  cossub  12273  demoivre  12305  eirraplem  12309  moddvds  12331  0dvds  12343  iddvdsexp  12347  dvdssub  12370  dvdsle  12376  dvdsleabs  12377  dvdseq  12380  dvdsflip  12383  mulsucdiv2z  12417  divalgb  12457  divalg2  12458  ndvdsadd  12463  bitsp1  12483  gcdneg  12524  gcdabs2  12532  modgcd  12533  bezoutlemsup  12551  gcdmultiplez  12563  gcdeq  12565  dvdssq  12573  lcmcllem  12610  lcmneg  12617  lcmdvds  12622  qredeu  12640  cncongrcoprm  12649  isprm3  12661  prmrp  12688  divnumden  12739  phiprmpw  12765  crth  12767  hashgcdlem  12781  hashgcdeq  12783  modprminv  12793  modprminveq  12794  modprmn0modprm0  12800  coprimeprodsq2  12802  pcpre1  12836  pccl  12843  pcmul  12845  pcdiv  12846  pcqcl  12850  pcexp  12853  pcdvds  12859  pcndvds  12861  pcndvds2  12863  pcelnn  12865  pcgcd1  12872  pc2dvds  12874  pc11  12875  gzsubcl  12924  4sqlem3  12934  setsresg  13091  pwssnf1o  13352  xpsfeq  13399  submcl  13533  grpinvnzcl  13626  mulgnnass  13715  nmzsubg  13768  nmznsg  13771  resghm2b  13820  ghmnsgpreima  13827  gsumfzsnfd  13903  iscrng2  13999  subrngpropd  14201  issubrg3  14232  subrgpropd  14238  islmodd  14278  lss1d  14368  lspsncl  14377  lspsnid  14392  df2idl2  14494  2idlcpbl  14509  qusrhm  14513  gsumfzfsumlemm  14572  iunopn  14697  unopn  14700  eltg  14747  eltg2  14748  tgcl  14759  tgiun  14768  tgidm  14769  isopn3i  14830  isneip  14841  neipsm  14849  restbasg  14863  restopn2  14878  lmbrf  14910  cnclima  14918  lmss  14941  txbasval  14962  txlm  14974  psmetxrge0  15027  blininf  15119  blssps  15122  blss  15123  elmopn2  15144  bdmet  15197  metrest  15201  bl2ioo  15245  dvcjbr  15403  plyaddlem1  15442  plymullem1  15443  plyreres  15459  dvply1  15460  dvply2g  15461  efper  15502  sinperlem  15503  abssinper  15541  cxpexprp  15590  logcxp  15592  rpcxpcl  15598  rpcxproot  15609  rprelogbmulexp  15651  lgsval2lem  15710  lgssq2  15741  lgsprme0  15742  ausgrusgrben  15987  bj-inex  16379  peano5set  16412  findset  16417  bj-findis  16451  nninfsellemsuc  16492  nninfself  16493  cvgcmp2nlemabs  16514  iooref1o  16516  trilpolemeq1  16522  nconstwlpolemgt0  16546