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  940  3adantr1  1159  3adantr2  1160  3adantr3  1161  syl3anr1  1302  syl3anr3  1304  dfbi3dc  1417  xordidc  1419  elabgt  2916  sbciegft  3031  csbtt  3107  csbnestgf  3148  copsex2t  4294  pofun  4364  onsucmin  4560  onsucelsucr  4561  onsucsssucr  4562  ordsucunielexmid  4584  ordsuc  4616  nlimsucg  4619  elnn  4659  xpsspw  4792  elxp4  5176  elxp5  5177  funimass2  5358  imain  5362  funimaexg  5364  f1ff1  5498  dff1o2  5536  resdif  5553  funbrfv  5627  fvelimab  5645  eqfnfv2  5688  fvimacnvi  5704  ffvresb  5753  fnressn  5780  fmptapd  5785  fnex  5816  rexima  5833  ralima  5834  f1elima  5852  fnotovb  5998  mpoeq12  6015  fovcdm  6099  fnovrn  6104  ofrfval  6177  ofvalg  6178  cofunexg  6204  cofunex2g  6205  mpoexxg  6306  mpoexg  6307  f1o2ndf1  6324  spc2ed  6329  smodm2  6391  tfrlem9  6415  tfrlemibxssdm  6423  tfr1onlembxssdm  6439  tfrcllembxssdm  6452  tfri3  6463  rdgtfr  6470  rdgruledefgg  6471  oav2  6559  oasuc  6560  omv2  6561  onasuc  6562  omsuc  6568  onmsuc  6569  nnaass  6581  nndi  6582  nndir  6586  nnaword  6607  ecelqsg  6685  iinerm  6704  ecovass  6741  ecoviass  6742  ecovdi  6743  ecovidi  6744  fvdiagfn  6790  ixpssmap2g  6824  domentr  6893  xpdom1g  6940  fopwdom  6945  ssenen  6960  phplem3  6963  phplem4  6964  php5dom  6972  ssfilem  6984  diffitest  6996  ctssdccl  7225  pm54.43  7310  addclpi  7453  addasspig  7456  mulasspig  7458  distrpig  7459  mulcanpig  7461  nnppipi  7469  enqdc1  7488  addassnqg  7508  ltbtwnnqq  7541  prarloclemarch  7544  prarloclemarch2  7545  enq0sym  7558  enq0ref  7559  addclnq0  7577  nqpnq0nq  7579  nnanq0  7584  distrnq0  7585  addassnq0lemcl  7587  addassnq0  7588  distnq0r  7589  prarloclemlt  7619  genpassl  7650  genpassu  7651  genpassg  7652  nqpru  7678  addcomprg  7704  mulcomprg  7706  distrlem1prl  7708  distrlem1pru  7709  1idprl  7716  1idpru  7717  recexprlemdisj  7756  recexprlem1ssl  7759  peano2nnnn  7979  ax1rid  8003  axcaucvglemcl  8021  le2tri3i  8194  add4  8246  cnegexlem1  8260  cnegexlem3  8262  cnegex  8263  subadd  8288  addsub  8296  addsubeq4  8300  negdi  8342  renegcl  8346  resubcl  8349  subdi  8470  mulneg2  8481  mul2neg  8483  submul2  8484  ltnegcon2  8550  lenegcon2  8553  lesub0  8565  cru  8688  recextlem1  8737  recexap  8739  div12ap  8780  divnegap  8792  letrp1  8934  dfinfre  9042  peano2nn  9061  nndivre  9085  nnsub  9088  nndivtr  9091  arch  9305  bndndx  9307  nn0addge1  9354  nn0addge2  9355  zaddcl  9425  zsubcl  9426  zltnle  9431  zrevaddcl  9436  nzadd  9438  zleltp1  9441  zltlem1  9443  zdiv  9474  peano2uz2  9493  uzind  9497  eluzp1l  9686  ublbneg  9747  qaddcl  9769  qsubcl  9772  qreccl  9776  qdivcl  9777  qrevaddcl  9778  irradd  9780  irrmul  9781  rerpdivcl  9819  nn0ledivnn  9902  xrre  9955  rexsub  9988  xaddass  10004  xnpcan  10007  xsubge0  10016  xposdif  10017  elioc2  10071  icoshft  10125  iccdil  10133  fzss2  10199  fzsuc2  10214  fzrev2  10220  elfzm11  10226  elfzp1b  10232  fzrevral  10240  fzshftral  10243  fzof  10279  fzoval  10283  fzon  10302  elfzoextl  10333  fzosubel  10336  zpnn0elfzo  10349  elfzom1b  10371  qltnle  10399  flqlt  10439  flqbi  10446  flqaddz  10453  fzofig  10590  seq3feq2  10634  ser3le  10695  expp1  10704  expm1t  10725  expeq0  10728  binom2sub  10811  bernneq  10818  expnlbnd  10822  zzlesq  10866  faccl  10893  facdiv  10896  bcpasc  10924  bccl  10925  ffz0hash  10991  fnfzo0hash  10993  wrdlen1  11044  wrdred1  11049  ccatval21sw  11075  wrdl1exs1  11097  ccatws1cl  11100  ccatws1leng  11102  pfxmpt  11145  pfxfv  11149  pfxfvlsw  11160  ccatpfx  11166  pfx1  11168  2shfti  11192  crim  11219  mulreap  11225  resub  11231  imsub  11239  ipcnval  11247  cjsub  11253  resqrexlemfp1  11370  resqrexlemgt0  11381  sqabsadd  11416  sqabssub  11417  abs2dif2  11468  cau3lem  11475  icodiamlt  11541  xrmaxaddlem  11621  clim  11642  clim2  11644  clim2c  11645  clim0c  11647  2clim  11662  climabs0  11668  climcn1  11669  climcn2  11670  climsqz  11696  climsqz2  11697  climub  11705  climserle  11706  fsum3cvg  11739  fisumss  11753  fsum3ser  11758  sumsplitdc  11793  fsump1i  11794  fsumlessfi  11821  telfsumo  11827  fsumparts  11831  iserabs  11836  binomlem  11844  isumsplit  11852  isum1p  11853  isumlessdc  11857  mertenslem2  11897  mertensabs  11898  prodfap0  11906  prodfrecap  11907  prodfdivap  11908  fproddccvg  11933  prodmodclem2  11938  fprodssdc  11951  fprodabs  11977  fprodeq0  11978  fprodeq0g  11999  ege2le3  12032  efsub  12042  efexp  12043  efsep  12052  sinsub  12101  cossub  12102  demoivre  12134  eirraplem  12138  moddvds  12160  0dvds  12172  iddvdsexp  12176  dvdssub  12199  dvdsle  12205  dvdsleabs  12206  dvdseq  12209  dvdsflip  12212  mulsucdiv2z  12246  divalgb  12286  divalg2  12287  ndvdsadd  12292  bitsp1  12312  gcdneg  12353  gcdabs2  12361  modgcd  12362  bezoutlemsup  12380  gcdmultiplez  12392  gcdeq  12394  dvdssq  12402  lcmcllem  12439  lcmneg  12446  lcmdvds  12451  qredeu  12469  cncongrcoprm  12478  isprm3  12490  prmrp  12517  divnumden  12568  phiprmpw  12594  crth  12596  hashgcdlem  12610  hashgcdeq  12612  modprminv  12622  modprminveq  12623  modprmn0modprm0  12629  coprimeprodsq2  12631  pcpre1  12665  pccl  12672  pcmul  12674  pcdiv  12675  pcqcl  12679  pcexp  12682  pcdvds  12688  pcndvds  12690  pcndvds2  12692  pcelnn  12694  pcgcd1  12701  pc2dvds  12703  pc11  12704  gzsubcl  12753  4sqlem3  12763  setsresg  12920  pwssnf1o  13180  xpsfeq  13227  submcl  13361  grpinvnzcl  13454  mulgnnass  13543  nmzsubg  13596  nmznsg  13599  resghm2b  13648  ghmnsgpreima  13655  gsumfzsnfd  13731  iscrng2  13827  subrngpropd  14028  issubrg3  14059  subrgpropd  14065  islmodd  14105  lss1d  14195  lspsncl  14204  lspsnid  14219  df2idl2  14321  2idlcpbl  14336  qusrhm  14340  gsumfzfsumlemm  14399  iunopn  14524  unopn  14527  eltg  14574  eltg2  14575  tgcl  14586  tgiun  14595  tgidm  14596  isopn3i  14657  isneip  14668  neipsm  14676  restbasg  14690  restopn2  14705  lmbrf  14737  cnclima  14745  lmss  14768  txbasval  14789  txlm  14801  psmetxrge0  14854  blininf  14946  blssps  14949  blss  14950  elmopn2  14971  bdmet  15024  metrest  15028  bl2ioo  15072  dvcjbr  15230  plyaddlem1  15269  plymullem1  15270  plyreres  15286  dvply1  15287  dvply2g  15288  efper  15329  sinperlem  15330  abssinper  15368  cxpexprp  15417  logcxp  15419  rpcxpcl  15425  rpcxproot  15436  rprelogbmulexp  15478  lgsval2lem  15537  lgssq2  15568  lgsprme0  15569  bj-inex  15957  peano5set  15990  findset  15995  bj-findis  16029  nninfsellemsuc  16064  nninfself  16065  cvgcmp2nlemabs  16086  iooref1o  16088  trilpolemeq1  16094  nconstwlpolemgt0  16118