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  3adantr1  1156  3adantr2  1157  3adantr3  1158  syl3anr1  1290  syl3anr3  1292  dfbi3dc  1397  xordidc  1399  elabgt  2879  sbciegft  2994  csbtt  3070  csbnestgf  3110  copsex2t  4246  pofun  4313  onsucmin  4507  onsucelsucr  4508  onsucsssucr  4509  ordsucunielexmid  4531  ordsuc  4563  nlimsucg  4566  elnn  4606  xpsspw  4739  elxp4  5117  elxp5  5118  funimass2  5295  imain  5299  funimaexg  5301  f1ff1  5430  dff1o2  5467  resdif  5484  funbrfv  5555  fvelimab  5573  eqfnfv2  5615  fvimacnvi  5631  ffvresb  5680  fnressn  5703  fmptapd  5708  fnex  5739  rexima  5756  ralima  5757  f1elima  5774  fnotovb  5918  mpoeq12  5935  fovcdm  6017  fnovrn  6022  ofrfval  6091  ofvalg  6092  cofunexg  6110  cofunex2g  6111  mpoexxg  6211  mpoexg  6212  f1o2ndf1  6229  spc2ed  6234  smodm2  6296  tfrlem9  6320  tfrlemibxssdm  6328  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  tfri3  6368  rdgtfr  6375  rdgruledefgg  6376  oav2  6464  oasuc  6465  omv2  6466  onasuc  6467  omsuc  6473  onmsuc  6474  nnaass  6486  nndi  6487  nndir  6491  nnaword  6512  ecelqsg  6588  iinerm  6607  ecovass  6644  ecoviass  6645  ecovdi  6646  ecovidi  6647  fvdiagfn  6693  ixpssmap2g  6727  domentr  6791  xpdom1g  6833  fopwdom  6836  ssenen  6851  phplem3  6854  phplem4  6855  php5dom  6863  ssfilem  6875  diffitest  6887  ctssdccl  7110  pm54.43  7189  addclpi  7326  addasspig  7329  mulasspig  7331  distrpig  7332  mulcanpig  7334  nnppipi  7342  enqdc1  7361  addassnqg  7381  ltbtwnnqq  7414  prarloclemarch  7417  prarloclemarch2  7418  enq0sym  7431  enq0ref  7432  addclnq0  7450  nqpnq0nq  7452  nnanq0  7457  distrnq0  7458  addassnq0lemcl  7460  addassnq0  7461  distnq0r  7462  prarloclemlt  7492  genpassl  7523  genpassu  7524  genpassg  7525  nqpru  7551  addcomprg  7577  mulcomprg  7579  distrlem1prl  7581  distrlem1pru  7582  1idprl  7589  1idpru  7590  recexprlemdisj  7629  recexprlem1ssl  7632  peano2nnnn  7852  ax1rid  7876  axcaucvglemcl  7894  le2tri3i  8066  add4  8118  cnegexlem1  8132  cnegexlem3  8134  cnegex  8135  subadd  8160  addsub  8168  addsubeq4  8172  negdi  8214  renegcl  8218  resubcl  8221  subdi  8342  mulneg2  8353  mul2neg  8355  submul2  8356  ltnegcon2  8421  lenegcon2  8424  lesub0  8436  cru  8559  recextlem1  8608  recexap  8610  div12ap  8651  divnegap  8663  letrp1  8805  dfinfre  8913  peano2nn  8931  nndivre  8955  nnsub  8958  nndivtr  8961  arch  9173  bndndx  9175  nn0addge1  9222  nn0addge2  9223  zaddcl  9293  zsubcl  9294  zltnle  9299  zrevaddcl  9303  nzadd  9305  zleltp1  9308  zltlem1  9310  zdiv  9341  peano2uz2  9360  uzind  9364  eluzp1l  9552  ublbneg  9613  qaddcl  9635  qsubcl  9638  qreccl  9642  qdivcl  9643  qrevaddcl  9644  irradd  9646  irrmul  9647  rerpdivcl  9684  nn0ledivnn  9767  xrre  9820  rexsub  9853  xaddass  9869  xnpcan  9872  xsubge0  9881  xposdif  9882  elioc2  9936  icoshft  9990  iccdil  9998  fzss2  10064  fzsuc2  10079  fzrev2  10085  elfzm11  10091  elfzp1b  10097  fzrevral  10105  fzshftral  10108  fzof  10144  fzoval  10148  fzon  10166  fzosubel  10194  zpnn0elfzo  10207  elfzom1b  10229  qltnle  10246  flqlt  10283  flqbi  10290  flqaddz  10297  fzofig  10432  seq3feq2  10470  ser3le  10518  expp1  10527  expm1t  10548  expeq0  10551  binom2sub  10634  bernneq  10641  expnlbnd  10645  faccl  10715  facdiv  10718  bcpasc  10746  bccl  10747  ffz0hash  10813  fnfzo0hash  10815  2shfti  10840  crim  10867  mulreap  10873  resub  10879  imsub  10887  ipcnval  10895  cjsub  10901  resqrexlemfp1  11018  resqrexlemgt0  11029  sqabsadd  11064  sqabssub  11065  abs2dif2  11116  cau3lem  11123  icodiamlt  11189  xrmaxaddlem  11268  clim  11289  clim2  11291  clim2c  11292  clim0c  11294  2clim  11309  climabs0  11315  climcn1  11316  climcn2  11317  climsqz  11343  climsqz2  11344  climub  11352  climserle  11353  fsum3cvg  11386  fisumss  11400  fsum3ser  11405  sumsplitdc  11440  fsump1i  11441  fsumlessfi  11468  telfsumo  11474  fsumparts  11478  iserabs  11483  binomlem  11491  isumsplit  11499  isum1p  11500  isumlessdc  11504  mertenslem2  11544  mertensabs  11545  prodfap0  11553  prodfrecap  11554  prodfdivap  11555  fproddccvg  11580  prodmodclem2  11585  fprodssdc  11598  fprodabs  11624  fprodeq0  11625  fprodeq0g  11646  ege2le3  11679  efsub  11689  efexp  11690  efsep  11699  sinsub  11748  cossub  11749  demoivre  11780  eirraplem  11784  moddvds  11806  0dvds  11818  iddvdsexp  11822  dvdssub  11845  dvdsle  11850  dvdsleabs  11851  dvdseq  11854  dvdsflip  11857  mulsucdiv2z  11890  divalgb  11930  divalg2  11931  ndvdsadd  11936  gcdneg  11983  gcdabs2  11991  modgcd  11992  bezoutlemsup  12010  gcdmultiplez  12022  gcdeq  12024  dvdssq  12032  lcmcllem  12067  lcmneg  12074  lcmdvds  12079  qredeu  12097  cncongrcoprm  12106  isprm3  12118  prmrp  12145  divnumden  12196  phiprmpw  12222  crth  12224  hashgcdlem  12238  hashgcdeq  12239  modprminv  12249  modprminveq  12250  modprmn0modprm0  12256  coprimeprodsq2  12258  pcpre1  12292  pccl  12299  pcmul  12301  pcdiv  12302  pcqcl  12306  pcexp  12309  pcdvds  12314  pcndvds  12316  pcndvds2  12318  pcelnn  12320  pcgcd1  12327  pc2dvds  12329  pc11  12330  gzsubcl  12378  4sqlem3  12388  setsresg  12500  xpsfeq  12764  submcl  12870  grpinvnzcl  12942  mulgnnass  13018  nmzsubg  13070  nmznsg  13073  iscrng2  13198  issubrg3  13368  subrgpropd  13369  islmodd  13383  iunopn  13505  unopn  13508  eltg  13555  eltg2  13556  tgcl  13567  tgiun  13576  tgidm  13577  isopn3i  13638  isneip  13649  neipsm  13657  restbasg  13671  restopn2  13686  lmbrf  13718  cnclima  13726  lmss  13749  txbasval  13770  txlm  13782  psmetxrge0  13835  blininf  13927  blssps  13930  blss  13931  elmopn2  13952  bdmet  14005  metrest  14009  bl2ioo  14045  dvcjbr  14175  efper  14231  sinperlem  14232  abssinper  14270  cxpexprp  14319  logcxp  14321  rpcxpcl  14327  rpcxproot  14337  rprelogbmulexp  14377  lgsval2lem  14414  lgssq2  14445  lgsprme0  14446  bj-inex  14662  peano5set  14695  findset  14700  bj-findis  14734  nninfsellemsuc  14764  nninfself  14765  cvgcmp2nlemabs  14783  iooref1o  14785  trilpolemeq1  14791  nconstwlpolemgt0  14814