Theorem sylan2 284

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 275	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylan2.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	syldan 280	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylan2b  285  sylan2br  286  syl2an  287  sylanr1  402  sylanr2  403  mpanr2  435  adantrl  470  adantrr  471  ancom2s  556  3adantr1  1146  3adantr2  1147  3adantr3  1148  syl3anr1  1280  syl3anr3  1282  dfbi3dc  1387  xordidc  1389  elabgt  2866  sbciegft  2980  csbtt  3056  csbnestgf  3096  copsex2t  4222  pofun  4289  onsucmin  4483  onsucelsucr  4484  onsucsssucr  4485  ordsucunielexmid  4507  ordsuc  4539  nlimsucg  4542  elnn  4582  xpsspw  4715  elxp4  5090  elxp5  5091  funimass2  5265  imain  5269  funimaexg  5271  f1ff1  5400  dff1o2  5436  resdif  5453  funbrfv  5524  fvelimab  5541  eqfnfv2  5583  fvimacnvi  5598  ffvresb  5647  fnressn  5670  fmptapd  5675  fnex  5706  rexima  5722  ralima  5723  f1elima  5740  fnotovb  5881  mpoeq12  5898  fovrn  5980  fnovrn  5985  ofrfval  6057  ofvalg  6058  cofunexg  6076  cofunex2g  6077  mpoexxg  6175  mpoexg  6176  f1o2ndf1  6192  spc2ed  6197  smodm2  6259  tfrlem9  6283  tfrlemibxssdm  6291  tfr1onlembxssdm  6307  tfrcllembxssdm  6320  tfri3  6331  rdgtfr  6338  rdgruledefgg  6339  oav2  6427  oasuc  6428  omv2  6429  onasuc  6430  omsuc  6436  onmsuc  6437  nnaass  6449  nndi  6450  nndir  6454  nnaword  6475  ecelqsg  6550  iinerm  6569  ecovass  6606  ecoviass  6607  ecovdi  6608  ecovidi  6609  fvdiagfn  6655  ixpssmap2g  6689  domentr  6753  xpdom1g  6795  fopwdom  6798  ssenen  6813  phplem3  6816  phplem4  6817  php5dom  6825  ssfilem  6837  diffitest  6849  ctssdccl  7072  pm54.43  7142  addclpi  7264  addasspig  7267  mulasspig  7269  distrpig  7270  mulcanpig  7272  nnppipi  7280  enqdc1  7299  addassnqg  7319  ltbtwnnqq  7352  prarloclemarch  7355  prarloclemarch2  7356  enq0sym  7369  enq0ref  7370  addclnq0  7388  nqpnq0nq  7390  nnanq0  7395  distrnq0  7396  addassnq0lemcl  7398  addassnq0  7399  distnq0r  7400  prarloclemlt  7430  genpassl  7461  genpassu  7462  genpassg  7463  nqpru  7489  addcomprg  7515  mulcomprg  7517  distrlem1prl  7519  distrlem1pru  7520  1idprl  7527  1idpru  7528  recexprlemdisj  7567  recexprlem1ssl  7570  peano2nnnn  7790  ax1rid  7814  axcaucvglemcl  7832  le2tri3i  8003  add4  8055  cnegexlem1  8069  cnegexlem3  8071  cnegex  8072  subadd  8097  addsub  8105  addsubeq4  8109  negdi  8151  renegcl  8155  resubcl  8158  subdi  8279  mulneg2  8290  mul2neg  8292  submul2  8293  ltnegcon2  8358  lenegcon2  8361  lesub0  8373  cru  8496  recextlem1  8544  recexap  8546  div12ap  8586  divnegap  8598  letrp1  8739  dfinfre  8847  peano2nn  8865  nndivre  8889  nnsub  8892  nndivtr  8895  arch  9107  bndndx  9109  nn0addge1  9156  nn0addge2  9157  zaddcl  9227  zsubcl  9228  zltnle  9233  zrevaddcl  9237  nzadd  9239  zleltp1  9242  zltlem1  9244  zdiv  9275  peano2uz2  9294  uzind  9298  eluzp1l  9486  ublbneg  9547  qaddcl  9569  qsubcl  9572  qreccl  9576  qdivcl  9577  qrevaddcl  9578  irradd  9580  irrmul  9581  rerpdivcl  9616  nn0ledivnn  9699  xrre  9752  rexsub  9785  xaddass  9801  xnpcan  9804  xsubge0  9813  xposdif  9814  elioc2  9868  icoshft  9922  iccdil  9930  fzss2  9995  fzsuc2  10010  fzrev2  10016  elfzm11  10022  elfzp1b  10028  fzrevral  10036  fzshftral  10039  fzof  10075  fzoval  10079  fzon  10097  fzosubel  10125  zpnn0elfzo  10138  elfzom1b  10160  qltnle  10177  flqlt  10214  flqbi  10221  flqaddz  10228  fzofig  10363  seq3feq2  10401  ser3le  10449  expp1  10458  expm1t  10479  expeq0  10482  binom2sub  10564  bernneq  10571  expnlbnd  10575  faccl  10644  facdiv  10647  bcpasc  10675  bccl  10676  ffz0hash  10742  fnfzo0hash  10744  2shfti  10769  crim  10796  mulreap  10802  resub  10808  imsub  10816  ipcnval  10824  cjsub  10830  resqrexlemfp1  10947  resqrexlemgt0  10958  sqabsadd  10993  sqabssub  10994  abs2dif2  11045  cau3lem  11052  icodiamlt  11118  xrmaxaddlem  11197  clim  11218  clim2  11220  clim2c  11221  clim0c  11223  2clim  11238  climabs0  11244  climcn1  11245  climcn2  11246  climsqz  11272  climsqz2  11273  climub  11281  climserle  11282  fsum3cvg  11315  fisumss  11329  fsum3ser  11334  sumsplitdc  11369  fsump1i  11370  fsumlessfi  11397  telfsumo  11403  fsumparts  11407  iserabs  11412  binomlem  11420  isumsplit  11428  isum1p  11429  isumlessdc  11433  mertenslem2  11473  mertensabs  11474  prodfap0  11482  prodfrecap  11483  prodfdivap  11484  fproddccvg  11509  prodmodclem2  11514  fprodssdc  11527  fprodabs  11553  fprodeq0  11554  fprodeq0g  11575  ege2le3  11608  efsub  11618  efexp  11619  efsep  11628  sinsub  11677  cossub  11678  demoivre  11709  eirraplem  11713  moddvds  11735  0dvds  11747  iddvdsexp  11751  dvdssub  11774  dvdsle  11778  dvdsleabs  11779  dvdseq  11782  dvdsflip  11785  mulsucdiv2z  11818  divalgb  11858  divalg2  11859  ndvdsadd  11864  gcdneg  11911  gcdabs2  11919  modgcd  11920  bezoutlemsup  11938  gcdmultiplez  11950  gcdeq  11952  dvdssq  11960  lcmcllem  11995  lcmneg  12002  lcmdvds  12007  qredeu  12025  cncongrcoprm  12034  isprm3  12046  prmrp  12073  divnumden  12124  phiprmpw  12150  crth  12152  hashgcdlem  12166  hashgcdeq  12167  modprminv  12177  modprminveq  12178  modprmn0modprm0  12184  coprimeprodsq2  12186  pcpre1  12220  pccl  12227  pcmul  12229  pcdiv  12230  pcqcl  12234  pcexp  12237  pcdvds  12242  pcndvds  12244  pcndvds2  12246  pcelnn  12248  pcgcd1  12255  pc2dvds  12257  pc11  12258  gzsubcl  12306  4sqlem3  12316  setsresg  12428  iunopn  12600  unopn  12603  eltg  12652  eltg2  12653  tgcl  12664  tgiun  12673  tgidm  12674  isopn3i  12735  isneip  12746  neipsm  12754  restbasg  12768  restopn2  12783  lmbrf  12815  cnclima  12823  lmss  12846  txbasval  12867  txlm  12879  psmetxrge0  12932  blininf  13024  blssps  13027  blss  13028  elmopn2  13049  bdmet  13102  metrest  13106  bl2ioo  13142  dvcjbr  13272  efper  13328  sinperlem  13329  abssinper  13367  cxpexprp  13416  logcxp  13418  rpcxpcl  13424  rpcxproot  13434  rprelogbmulexp  13474  lgsval2lem  13511  lgssq2  13542  lgsprme0  13543  bj-inex  13749  peano5set  13782  findset  13787  bj-findis  13821  nninfsellemsuc  13852  nninfself  13853  cvgcmp2nlemabs  13871  iooref1o  13873  trilpolemeq1  13879  nconstwlpolemgt0  13902