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  2957  sbciegft  3072  csbtt  3149  csbnestgf  3190  copsex2t  4360  pofun  4432  onsucmin  4628  onsucelsucr  4629  onsucsssucr  4630  ordsucunielexmid  4652  ordsuc  4684  nlimsucg  4687  elnn  4727  xpsspw  4861  elxp4  5249  elxp5  5250  funimass2  5433  imain  5437  funimaexg  5439  f1ff1  5580  dff1o2  5618  resdif  5635  funbrfv  5712  fnbrfvb2  5718  fvelimab  5732  eqfnfv2  5775  fvimacnvi  5791  ffvresb  5839  fnressn  5869  fmptapd  5874  fnex  5905  rexima  5926  ralima  5927  f1elima  5945  fnotovb  6095  mpoeq12  6112  fovcdm  6196  fnovrn  6201  ofrfval  6274  ofvalg  6275  cofunexg  6301  cofunex2g  6302  mpoexxg  6405  mpoexg  6406  f1o2ndf1  6423  spc2ed  6428  funsssuppss  6457  smodm2  6525  tfrlem9  6549  tfrlemibxssdm  6557  tfr1onlembxssdm  6573  tfrcllembxssdm  6586  tfri3  6597  rdgtfr  6604  rdgruledefgg  6605  oav2  6695  oasuc  6696  omv2  6697  onasuc  6698  omsuc  6704  onmsuc  6705  nnaass  6717  nndi  6718  nndir  6722  nnaword  6743  ecelqsg  6821  iinerm  6840  ecovass  6877  ecoviass  6878  ecovdi  6879  ecovidi  6880  fvdiagfn  6927  ixpssmap2g  6961  domentr  7030  xpdom1g  7083  fopwdom  7088  ssenen  7104  phplem3  7107  phplem4  7108  php5dom  7116  ssfilem  7129  ssfilemd  7131  diffitest  7143  ctssdccl  7401  pm54.43  7486  pw1if  7534  addclpi  7641  addasspig  7644  mulasspig  7646  distrpig  7647  mulcanpig  7649  nnppipi  7657  enqdc1  7676  addassnqg  7696  ltbtwnnqq  7729  prarloclemarch  7732  prarloclemarch2  7733  enq0sym  7746  enq0ref  7747  addclnq0  7765  nqpnq0nq  7767  nnanq0  7772  distrnq0  7773  addassnq0lemcl  7775  addassnq0  7776  distnq0r  7777  prarloclemlt  7807  genpassl  7838  genpassu  7839  genpassg  7840  nqpru  7866  addcomprg  7892  mulcomprg  7894  distrlem1prl  7896  distrlem1pru  7897  1idprl  7904  1idpru  7905  recexprlemdisj  7944  recexprlem1ssl  7947  peano2nnnn  8167  ax1rid  8191  axcaucvglemcl  8209  le2tri3i  8381  add4  8433  cnegexlem1  8447  cnegexlem3  8449  cnegex  8450  subadd  8475  addsub  8483  addsubeq4  8487  negdi  8529  renegcl  8533  resubcl  8536  subdi  8657  mulneg2  8668  mul2neg  8670  submul2  8671  ltnegcon2  8737  lenegcon2  8740  lesub0  8752  cru  8875  recextlem1  8924  recexap  8926  div12ap  8967  divnegap  8979  letrp1  9121  dfinfre  9229  peano2nn  9248  nndivre  9272  nnsub  9275  nndivtr  9278  arch  9492  bndndx  9494  nn0addge1  9541  nn0addge2  9542  zaddcl  9616  zsubcl  9617  zltnle  9622  zrevaddcl  9627  nzadd  9629  zleltp1  9632  zltlem1  9634  zdiv  9665  peano2uz2  9684  uzind  9688  eluzp1l  9878  ublbneg  9944  qaddcl  9966  qsubcl  9969  qreccl  9973  qdivcl  9974  qrevaddcl  9975  irradd  9977  irrmul  9978  rerpdivcl  10016  nn0ledivnn  10099  xrre  10152  rexsub  10185  xaddass  10201  xnpcan  10204  xsubge0  10213  xposdif  10214  elioc2  10268  icoshft  10322  iccdil  10330  fzss2  10397  fzsuc2  10412  fzrev2  10418  elfzm11  10424  elfzp1b  10430  fzrevral  10438  fzshftral  10441  fzof  10477  fzoval  10481  fzon  10500  elfzoextl  10535  fzosubel  10538  zpnn0elfzo  10551  elfzom1b  10573  qltnle  10602  flqlt  10642  flqbi  10649  flqaddz  10656  fzofig  10793  seq3feq2  10837  ser3le  10898  expp1  10907  expm1t  10928  expeq0  10931  binom2sub  11014  bernneq  11021  expnlbnd  11025  zzlesq  11069  faccl  11096  facdiv  11099  bcpasc  11127  bccl  11128  ffz0hash  11196  fnfzo0hash  11198  hashfibclem  11202  wrdlen1  11258  wrdred1  11263  ccatval21sw  11289  wrdl1exs1  11313  ccatws1cl  11316  ccatws1leng  11318  pfxmpt  11368  pfxfv  11372  pfxfvlsw  11383  ccatpfx  11389  pfx1  11391  swrdccatin1  11413  swrdccat  11423  pfxccatpfx1  11424  2shfti  11512  crim  11539  mulreap  11545  resub  11551  imsub  11559  ipcnval  11567  cjsub  11573  resqrexlemfp1  11690  resqrexlemgt0  11701  sqabsadd  11736  sqabssub  11737  abs2dif2  11788  cau3lem  11795  icodiamlt  11861  xrmaxaddlem  11941  clim  11962  clim2  11964  clim2c  11965  clim0c  11967  2clim  11982  climabs0  11988  climcn1  11989  climcn2  11990  climsqz  12016  climsqz2  12017  climub  12025  climserle  12026  fsum3cvg  12060  fisumss  12074  fsum3ser  12079  sumsplitdc  12114  fsump1i  12115  fsumlessfi  12142  telfsumo  12148  fsumparts  12152  iserabs  12157  binomlem  12165  isumsplit  12173  isum1p  12174  isumlessdc  12178  mertenslem2  12218  mertensabs  12219  prodfap0  12227  prodfrecap  12228  prodfdivap  12229  fproddccvg  12254  prodmodclem2  12259  fprodssdc  12272  fprodabs  12298  fprodeq0  12299  fprodeq0g  12320  ege2le3  12353  efsub  12363  efexp  12364  efsep  12373  sinsub  12422  cossub  12423  demoivre  12455  eirraplem  12459  moddvds  12481  0dvds  12493  iddvdsexp  12497  dvdssub  12520  dvdsle  12526  dvdsleabs  12527  dvdseq  12530  dvdsflip  12533  mulsucdiv2z  12567  divalgb  12607  divalg2  12608  ndvdsadd  12613  bitsp1  12633  gcdneg  12674  gcdabs2  12682  modgcd  12683  bezoutlemsup  12701  gcdmultiplez  12713  gcdeq  12715  dvdssq  12723  lcmcllem  12760  lcmneg  12767  lcmdvds  12772  qredeu  12790  cncongrcoprm  12799  isprm3  12811  prmrp  12838  divnumden  12889  phiprmpw  12915  crth  12917  hashgcdlem  12931  hashgcdeq  12933  modprminv  12943  modprminveq  12944  modprmn0modprm0  12950  coprimeprodsq2  12952  pcpre1  12986  pccl  12993  pcmul  12995  pcdiv  12996  pcqcl  13000  pcexp  13003  pcdvds  13009  pcndvds  13011  pcndvds2  13013  pcelnn  13015  pcgcd1  13022  pc2dvds  13024  pc11  13025  gzsubcl  13074  4sqlem3  13084  setsresg  13242  pwssnf1o  13503  xpsfeq  13550  submcl  13684  grpinvnzcl  13777  mulgnnass  13866  nmzsubg  13919  nmznsg  13922  resghm2b  13971  ghmnsgpreima  13978  gsumfzsnfd  14054  iscrng2  14151  subrngpropd  14353  issubrg3  14384  subrgpropd  14390  islmodd  14433  lss1d  14523  lspsncl  14532  lspsnid  14547  df2idl2  14649  2idlcpbl  14664  qusrhm  14668  gsumfzfsumlemm  14727  iunopn  14859  unopn  14862  eltg  14909  eltg2  14910  tgcl  14921  tgiun  14930  tgidm  14931  isopn3i  14992  isneip  15003  neipsm  15011  restbasg  15025  restopn2  15040  lmbrf  15072  cnclima  15080  lmss  15103  txbasval  15124  txlm  15136  psmetxrge0  15189  blininf  15281  blssps  15284  blss  15285  elmopn2  15306  bdmet  15359  metrest  15363  bl2ioo  15407  dvcjbr  15565  plyaddlem1  15604  plymullem1  15605  plyreres  15621  dvply1  15622  dvply2g  15623  efper  15664  sinperlem  15665  abssinper  15703  cxpexprp  15752  logcxp  15754  rpcxpcl  15760  rpcxproot  15771  rprelogbmulexp  15813  lgsval2lem  15875  lgssq2  15906  lgsprme0  15907  ausgrusgrben  16155  wlkepvtx  16362  bj-inex  16669  peano5set  16702  findset  16707  bj-findis  16741  nninfsellemsuc  16782  nninfself  16783  cvgcmp2nlemabs  16808  iooref1o  16810  trilpolemeq1  16816  nconstwlpolemgt0  16841