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 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  408  sylanr2  409  mpanr2  442  adantrl  482  adantrr  483  ancom2s  572  annimdc  950  ifpnst  1001  3adantr1  1187  3adantr2  1188  3adantr3  1189  syl3anr1  1330  syl3anr3  1332  dfbi3dc  1446  xordidc  1448  elabgt  2967  sbciegft  3082  csbtt  3159  csbnestgf  3200  copsex2t  4385  pofun  4457  onsucmin  4654  onsucelsucr  4655  onsucsssucr  4656  ordsucunielexmid  4678  ordsuc  4710  nlimsucg  4713  elnn  4753  xpsspw  4887  elxp4  5275  elxp5  5276  funimass2  5459  imain  5463  funimaexg  5465  f1ff1  5606  dff1o2  5644  resdif  5661  funbrfv  5739  fnbrfvb2  5745  fvelimab  5759  eqfnfv2  5807  fvimacnvi  5823  ffvresb  5871  fnressn  5901  fmptapd  5906  fnex  5937  rexima  5960  ralima  5961  f1elima  5979  fnotovb  6131  mpoeq12  6148  fovcdm  6232  fnovrn  6237  ofrfval  6311  ofvalg  6312  cofunexg  6338  cofunex2g  6339  mpoexxg  6446  mpoexg  6447  f1o2ndf1  6464  spc2ed  6469  funsssuppss  6498  smodm2  6566  tfrlem9  6590  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  tfri3  6638  rdgtfr  6645  rdgruledefgg  6646  oav2  6736  oasuc  6737  omv2  6738  onasuc  6739  omsuc  6745  onmsuc  6746  nnaass  6758  nndi  6759  nndir  6763  nnaword  6784  ecelqsg  6862  iinerm  6881  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  fvdiagfn  6975  ixpssmap2g  7009  domentr  7078  xpdom1g  7131  fopwdom  7136  ssenen  7152  phplem3  7155  phplem4  7156  php5dom  7164  ssfilem  7177  ssfilemd  7179  diffitest  7191  ctssdccl  7451  pm54.43  7536  pw1if  7584  addclpi  7694  addasspig  7697  mulasspig  7699  distrpig  7700  mulcanpig  7702  nnppipi  7710  enqdc1  7729  addassnqg  7749  ltbtwnnqq  7782  prarloclemarch  7785  prarloclemarch2  7786  enq0sym  7799  enq0ref  7800  addclnq0  7818  nqpnq0nq  7820  nnanq0  7825  distrnq0  7826  addassnq0lemcl  7828  addassnq0  7829  distnq0r  7830  prarloclemlt  7860  genpassl  7891  genpassu  7892  genpassg  7893  nqpru  7919  addcomprg  7945  mulcomprg  7947  distrlem1prl  7949  distrlem1pru  7950  1idprl  7957  1idpru  7958  recexprlemdisj  7997  recexprlem1ssl  8000  peano2nnnn  8220  ax1rid  8244  axcaucvglemcl  8262  le2tri3i  8434  add4  8487  cnegexlem1  8501  cnegexlem3  8503  cnegex  8504  subadd  8529  addsub  8537  addsubeq4  8541  negdi  8583  renegcl  8587  resubcl  8590  subdi  8712  mulneg2  8723  mul2neg  8725  submul2  8726  ltnegcon2  8792  lenegcon2  8795  lesub0  8807  cru  8931  recextlem1  8980  recexap  8982  div12ap  9025  divnegap  9037  letrp1  9179  dfinfre  9287  peano2nn  9317  nndivre  9341  nnsub  9344  nndivtr  9347  arch  9562  bndndx  9564  nn0addge1  9611  nn0addge2  9612  zaddcl  9686  zsubcl  9687  zltnle  9692  zrevaddcl  9697  nzadd  9699  zleltp1  9702  zltlem1  9704  zdiv  9736  peano2uz2  9755  uzind  9759  eluzp1l  9949  ublbneg  10015  qaddcl  10037  qsubcl  10040  qreccl  10044  qdivcl  10045  qrevaddcl  10046  irradd  10048  irrmul  10049  rerpdivcl  10087  nn0ledivnn  10170  xrre  10224  rexsub  10257  xaddass  10273  xnpcan  10276  xsubge0  10285  xposdif  10286  elioc2  10340  icoshft  10394  iccdil  10402  fzss2  10472  fzsuc2  10488  fzrev2  10494  elfzm11  10500  elfzp1b  10506  fzrevral  10514  fzshftral  10517  fzof  10553  fzoval  10557  fzon  10576  elfzoextl  10611  fzosubel  10614  zpnn0elfzo  10627  elfzom1b  10649  qltnle  10680  flqlt  10720  flqbi  10727  flqaddz  10734  fzofig  10871  seq3feq2  10915  ser3le  10976  expp1  10985  expm1t  11006  expeq0  11009  binom2sub  11092  bernneq  11100  expnlbnd  11104  zzlesq  11148  faccl  11175  facdiv  11178  bcpasc  11206  bccl  11207  ffz0hash  11278  fnfzo0hash  11280  hashfibclem  11284  hashf1lem2  11288  wrdlen1  11344  wrdred1  11349  ccatval21sw  11375  wrdl1exs1  11399  ccatws1cl  11402  ccatws1leng  11404  pfxmpt  11454  pfxfv  11458  pfxfvlsw  11469  ccatpfx  11475  pfx1  11477  swrdccatin1  11499  swrdccat  11509  pfxccatpfx1  11510  2shfti  11598  crim  11625  mulreap  11631  resub  11637  imsub  11645  ipcnval  11653  cjsub  11659  resqrexlemfp1  11777  resqrexlemgt0  11788  sqabsadd  11823  sqabssub  11824  abs2dif2  11875  cau3lem  11882  icodiamlt  11948  xrmaxaddlem  12028  clim  12049  clim2  12051  clim2c  12052  clim0c  12054  2clim  12069  climabs0  12075  climcn1  12076  climcn2  12077  climsqz  12103  climsqz2  12104  climub  12112  climserle  12113  fsum3cvg  12147  fisumss  12161  fsum3ser  12166  sumsplitdc  12201  fsump1i  12202  fsumlessfi  12229  telfsumo  12235  fsumparts  12239  iserabs  12244  binomlem  12252  isumsplit  12260  isum1p  12261  isumlessdc  12265  mertenslem2  12305  mertensabs  12306  prodfap0  12314  prodfrecap  12315  prodfdivap  12316  fproddccvg  12341  prodmodclem2  12346  fprodssdc  12359  fprodabs  12385  fprodeq0  12386  fprodeq0g  12407  ege2le3  12440  efsub  12450  efexp  12451  efsep  12460  sinsub  12509  cossub  12510  demoivre  12542  eirraplem  12546  moddvds  12568  0dvds  12580  iddvdsexp  12584  dvdssub  12607  dvdsle  12613  dvdsleabs  12614  dvdseq  12617  dvdsflip  12620  mulsucdiv2z  12654  divalgb  12694  divalg2  12695  ndvdsadd  12700  bitsp1  12720  gcdneg  12761  gcdabs2  12769  modgcd  12770  bezoutlemsup  12788  gcdmultiplez  12800  gcdeq  12802  dvdssq  12810  lcmcllem  12847  lcmneg  12854  lcmdvds  12859  qredeu  12877  cncongrcoprm  12886  isprm3  12898  prmrp  12925  divnumden  12976  phiprmpw  13002  crth  13004  hashgcdlem  13018  hashgcdeq  13020  modprminv  13030  modprminveq  13031  modprmn0modprm0  13037  coprimeprodsq2  13039  pcpre1  13073  pccl  13080  pcmul  13082  pcdiv  13083  pcqcl  13087  pcexp  13090  pcdvds  13096  pcndvds  13098  pcndvds2  13100  pcelnn  13102  pcgcd1  13109  pc2dvds  13111  pc11  13112  gzsubcl  13161  4sqlem3  13171  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemodife  13242  ballotfilemfrceq  13274  setsresg  13392  xpsfeq  13668  submcl  13788  grpinvnzcl  13879  mulgnnass  13962  nmzsubg  14015  nmznsg  14018  resghm2b  14067  ghmnsgpreima  14074  gzsumsnfd  14149  pwssnf1o  14213  iscrng2  14321  subrngpropd  14526  issubrg3  14557  subrgpropd  14563  islmodd  14631  lss1d  14722  lspsncl  14731  lspsnid  14746  df2idl2  14848  2idlcpbl  14863  qusrhm  14867  iunopn  15105  unopn  15108  eltg  15155  eltg2  15156  tgcl  15167  tgiun  15176  tgidm  15177  isopn3i  15238  isneip  15249  neipsm  15257  restbasg  15271  restopn2  15286  lmbrf  15318  cnclima  15326  lmss  15349  txbasval  15370  txlm  15382  psmetxrge0  15435  blininf  15527  blssps  15530  blss  15531  elmopn2  15552  bdmet  15605  metrest  15609  bl2ioo  15653  dvcjbr  15811  plyaddlem1  15850  plymullem1  15851  plyreres  15867  dvply1  15868  dvply2g  15869  efper  15911  sinperlem  15912  abssinper  15950  cxpexprp  16003  logcxp  16005  rpcxpcl  16011  rpcxproot  16022  rprelogbmulexp  16064  log2tlbndlog2  16088  lgsval2lem  16141  lgssq2  16172  lgsprme0  16173  ausgrusgrben  16421  wlkepvtx  16628  bj-inex  16945  peano5set  16978  findset  16983  bj-findis  17017  nninfsellemsuc  17067  nninfself  17068  cvgcmp2nlemabs  17093  iooref1o  17095  trilpolemeq1  17101  nconstwlpolemgt0  17126