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  4331  pofun  4403  onsucmin  4599  onsucelsucr  4600  onsucsssucr  4601  ordsucunielexmid  4623  ordsuc  4655  nlimsucg  4658  elnn  4698  xpsspw  4831  elxp4  5216  elxp5  5217  funimass2  5399  imain  5403  funimaexg  5405  f1ff1  5541  dff1o2  5579  resdif  5596  funbrfv  5672  fnbrfvb2  5678  fvelimab  5692  eqfnfv2  5735  fvimacnvi  5751  ffvresb  5800  fnressn  5829  fmptapd  5834  fnex  5865  rexima  5884  ralima  5885  f1elima  5903  fnotovb  6053  mpoeq12  6070  fovcdm  6154  fnovrn  6159  ofrfval  6233  ofvalg  6234  cofunexg  6260  cofunex2g  6261  mpoexxg  6362  mpoexg  6363  f1o2ndf1  6380  spc2ed  6385  smodm2  6447  tfrlem9  6471  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  tfri3  6519  rdgtfr  6526  rdgruledefgg  6527  oav2  6617  oasuc  6618  omv2  6619  onasuc  6620  omsuc  6626  onmsuc  6627  nnaass  6639  nndi  6640  nndir  6644  nnaword  6665  ecelqsg  6743  iinerm  6762  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  fvdiagfn  6848  ixpssmap2g  6882  domentr  6951  xpdom1g  7000  fopwdom  7005  ssenen  7020  phplem3  7023  phplem4  7024  php5dom  7032  ssfilem  7045  diffitest  7057  ctssdccl  7286  pm54.43  7371  pw1if  7418  addclpi  7522  addasspig  7525  mulasspig  7527  distrpig  7528  mulcanpig  7530  nnppipi  7538  enqdc1  7557  addassnqg  7577  ltbtwnnqq  7610  prarloclemarch  7613  prarloclemarch2  7614  enq0sym  7627  enq0ref  7628  addclnq0  7646  nqpnq0nq  7648  nnanq0  7653  distrnq0  7654  addassnq0lemcl  7656  addassnq0  7657  distnq0r  7658  prarloclemlt  7688  genpassl  7719  genpassu  7720  genpassg  7721  nqpru  7747  addcomprg  7773  mulcomprg  7775  distrlem1prl  7777  distrlem1pru  7778  1idprl  7785  1idpru  7786  recexprlemdisj  7825  recexprlem1ssl  7828  peano2nnnn  8048  ax1rid  8072  axcaucvglemcl  8090  le2tri3i  8263  add4  8315  cnegexlem1  8329  cnegexlem3  8331  cnegex  8332  subadd  8357  addsub  8365  addsubeq4  8369  negdi  8411  renegcl  8415  resubcl  8418  subdi  8539  mulneg2  8550  mul2neg  8552  submul2  8553  ltnegcon2  8619  lenegcon2  8622  lesub0  8634  cru  8757  recextlem1  8806  recexap  8808  div12ap  8849  divnegap  8861  letrp1  9003  dfinfre  9111  peano2nn  9130  nndivre  9154  nnsub  9157  nndivtr  9160  arch  9374  bndndx  9376  nn0addge1  9423  nn0addge2  9424  zaddcl  9494  zsubcl  9495  zltnle  9500  zrevaddcl  9505  nzadd  9507  zleltp1  9510  zltlem1  9512  zdiv  9543  peano2uz2  9562  uzind  9566  eluzp1l  9755  ublbneg  9816  qaddcl  9838  qsubcl  9841  qreccl  9845  qdivcl  9846  qrevaddcl  9847  irradd  9849  irrmul  9850  rerpdivcl  9888  nn0ledivnn  9971  xrre  10024  rexsub  10057  xaddass  10073  xnpcan  10076  xsubge0  10085  xposdif  10086  elioc2  10140  icoshft  10194  iccdil  10202  fzss2  10268  fzsuc2  10283  fzrev2  10289  elfzm11  10295  elfzp1b  10301  fzrevral  10309  fzshftral  10312  fzof  10348  fzoval  10352  fzon  10371  elfzoextl  10405  fzosubel  10408  zpnn0elfzo  10421  elfzom1b  10443  qltnle  10471  flqlt  10511  flqbi  10518  flqaddz  10525  fzofig  10662  seq3feq2  10706  ser3le  10767  expp1  10776  expm1t  10797  expeq0  10800  binom2sub  10883  bernneq  10890  expnlbnd  10894  zzlesq  10938  faccl  10965  facdiv  10968  bcpasc  10996  bccl  10997  ffz0hash  11063  fnfzo0hash  11065  wrdlen1  11117  wrdred1  11122  ccatval21sw  11148  wrdl1exs1  11170  ccatws1cl  11173  ccatws1leng  11175  pfxmpt  11220  pfxfv  11224  pfxfvlsw  11235  ccatpfx  11241  pfx1  11243  swrdccatin1  11265  swrdccat  11275  pfxccatpfx1  11276  2shfti  11350  crim  11377  mulreap  11383  resub  11389  imsub  11397  ipcnval  11405  cjsub  11411  resqrexlemfp1  11528  resqrexlemgt0  11539  sqabsadd  11574  sqabssub  11575  abs2dif2  11626  cau3lem  11633  icodiamlt  11699  xrmaxaddlem  11779  clim  11800  clim2  11802  clim2c  11803  clim0c  11805  2clim  11820  climabs0  11826  climcn1  11827  climcn2  11828  climsqz  11854  climsqz2  11855  climub  11863  climserle  11864  fsum3cvg  11897  fisumss  11911  fsum3ser  11916  sumsplitdc  11951  fsump1i  11952  fsumlessfi  11979  telfsumo  11985  fsumparts  11989  iserabs  11994  binomlem  12002  isumsplit  12010  isum1p  12011  isumlessdc  12015  mertenslem2  12055  mertensabs  12056  prodfap0  12064  prodfrecap  12065  prodfdivap  12066  fproddccvg  12091  prodmodclem2  12096  fprodssdc  12109  fprodabs  12135  fprodeq0  12136  fprodeq0g  12157  ege2le3  12190  efsub  12200  efexp  12201  efsep  12210  sinsub  12259  cossub  12260  demoivre  12292  eirraplem  12296  moddvds  12318  0dvds  12330  iddvdsexp  12334  dvdssub  12357  dvdsle  12363  dvdsleabs  12364  dvdseq  12367  dvdsflip  12370  mulsucdiv2z  12404  divalgb  12444  divalg2  12445  ndvdsadd  12450  bitsp1  12470  gcdneg  12511  gcdabs2  12519  modgcd  12520  bezoutlemsup  12538  gcdmultiplez  12550  gcdeq  12552  dvdssq  12560  lcmcllem  12597  lcmneg  12604  lcmdvds  12609  qredeu  12627  cncongrcoprm  12636  isprm3  12648  prmrp  12675  divnumden  12726  phiprmpw  12752  crth  12754  hashgcdlem  12768  hashgcdeq  12770  modprminv  12780  modprminveq  12781  modprmn0modprm0  12787  coprimeprodsq2  12789  pcpre1  12823  pccl  12830  pcmul  12832  pcdiv  12833  pcqcl  12837  pcexp  12840  pcdvds  12846  pcndvds  12848  pcndvds2  12850  pcelnn  12852  pcgcd1  12859  pc2dvds  12861  pc11  12862  gzsubcl  12911  4sqlem3  12921  setsresg  13078  pwssnf1o  13339  xpsfeq  13386  submcl  13520  grpinvnzcl  13613  mulgnnass  13702  nmzsubg  13755  nmznsg  13758  resghm2b  13807  ghmnsgpreima  13814  gsumfzsnfd  13890  iscrng2  13986  subrngpropd  14188  issubrg3  14219  subrgpropd  14225  islmodd  14265  lss1d  14355  lspsncl  14364  lspsnid  14379  df2idl2  14481  2idlcpbl  14496  qusrhm  14500  gsumfzfsumlemm  14559  iunopn  14684  unopn  14687  eltg  14734  eltg2  14735  tgcl  14746  tgiun  14755  tgidm  14756  isopn3i  14817  isneip  14828  neipsm  14836  restbasg  14850  restopn2  14865  lmbrf  14897  cnclima  14905  lmss  14928  txbasval  14949  txlm  14961  psmetxrge0  15014  blininf  15106  blssps  15109  blss  15110  elmopn2  15131  bdmet  15184  metrest  15188  bl2ioo  15232  dvcjbr  15390  plyaddlem1  15429  plymullem1  15430  plyreres  15446  dvply1  15447  dvply2g  15448  efper  15489  sinperlem  15490  abssinper  15528  cxpexprp  15577  logcxp  15579  rpcxpcl  15585  rpcxproot  15596  rprelogbmulexp  15638  lgsval2lem  15697  lgssq2  15728  lgsprme0  15729  ausgrusgrben  15974  bj-inex  16294  peano5set  16327  findset  16332  bj-findis  16366  nninfsellemsuc  16408  nninfself  16409  cvgcmp2nlemabs  16430  iooref1o  16432  trilpolemeq1  16438  nconstwlpolemgt0  16462