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  4387  pofun  4459  onsucmin  4656  onsucelsucr  4657  onsucsssucr  4658  ordsucunielexmid  4680  ordsuc  4712  nlimsucg  4715  elnn  4755  xpsspw  4889  elxp4  5278  elxp5  5279  funimass2  5462  imain  5466  funimaexg  5468  f1ff1  5609  dff1o2  5647  resdif  5664  funbrfv  5742  fnbrfvb2  5748  fvelimab  5762  eqfnfv2  5810  fvimacnvi  5826  ffvresb  5874  fnressn  5904  fmptapd  5909  fnex  5940  rexima  5963  ralima  5964  f1elima  5982  fnotovb  6134  mpoeq12  6151  fovcdm  6235  fnovrn  6240  ofrfval  6315  ofvalg  6316  cofunexg  6342  cofunex2g  6343  mpoexxg  6450  mpoexg  6451  f1o2ndf1  6468  spc2ed  6473  funsssuppss  6502  smodm2  6570  tfrlem9  6594  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  tfri3  6642  rdgtfr  6649  rdgruledefgg  6650  oav2  6740  oasuc  6741  omv2  6742  onasuc  6743  omsuc  6749  onmsuc  6750  nnaass  6762  nndi  6763  nndir  6767  nnaword  6788  ecelqsg  6866  iinerm  6885  ecovass  6922  ecoviass  6923  ecovdi  6924  ecovidi  6925  fvdiagfn  6979  ixpssmap2g  7013  domentr  7082  xpdom1g  7135  fopwdom  7140  ssenen  7156  phplem3  7159  phplem4  7160  php5dom  7168  ssfilem  7181  ssfilemd  7183  diffitest  7195  ctssdccl  7457  pm54.43  7542  pw1if  7590  addclpi  7700  addasspig  7703  mulasspig  7705  distrpig  7706  mulcanpig  7708  nnppipi  7716  enqdc1  7735  addassnqg  7755  ltbtwnnqq  7788  prarloclemarch  7791  prarloclemarch2  7792  enq0sym  7805  enq0ref  7806  addclnq0  7824  nqpnq0nq  7826  nnanq0  7831  distrnq0  7832  addassnq0lemcl  7834  addassnq0  7835  distnq0r  7836  prarloclemlt  7866  genpassl  7897  genpassu  7898  genpassg  7899  nqpru  7925  addcomprg  7951  mulcomprg  7953  distrlem1prl  7955  distrlem1pru  7956  1idprl  7963  1idpru  7964  recexprlemdisj  8003  recexprlem1ssl  8006  peano2nnnn  8226  ax1rid  8250  axcaucvglemcl  8268  le2tri3i  8441  add4  8494  cnegexlem1  8508  cnegexlem3  8510  cnegex  8511  subadd  8536  addsub  8544  addsubeq4  8548  negdi  8590  renegcl  8594  resubcl  8597  subdi  8719  mulneg2  8730  mul2neg  8732  submul2  8733  ltnegcon2  8799  lenegcon2  8802  lesub0  8814  cru  8938  recextlem1  8987  recexap  8989  div12ap  9032  divnegap  9044  letrp1  9186  dfinfre  9294  peano2nn  9325  nndivre  9349  nnsub  9352  nndivtr  9355  arch  9571  bndndx  9573  nn0addge1  9620  nn0addge2  9621  zaddcl  9695  zsubcl  9696  zltnle  9701  zrevaddcl  9706  nzadd  9708  zleltp1  9711  zltlem1  9713  zdiv  9745  peano2uz2  9764  uzind  9768  eluzp1l  9963  ublbneg  10029  qaddcl  10051  qsubcl  10054  qreccl  10058  qdivcl  10059  qrevaddcl  10060  irradd  10062  irrmul  10064  rerpdivcl  10102  nn0ledivnn  10185  xrre  10239  rexsub  10272  xaddass  10288  xnpcan  10291  xsubge0  10300  xposdif  10301  elioc2  10355  icoshft  10409  iccdil  10417  fzss2  10487  fzsuc2  10503  fzrev2  10509  elfzm11  10515  elfzp1b  10521  fzrevral  10529  fzshftral  10532  fzof  10568  fzoval  10572  fzon  10591  elfzoextl  10626  fzosubel  10629  zpnn0elfzo  10642  elfzom1b  10664  qltnle  10695  flapcl  10728  flaplelt  10730  flqlt  10738  flqbi  10746  flqaddz  10753  fzofig  10890  seq3feq2  10934  ser3le  10995  expp1  11004  expm1t  11025  expeq0  11028  binom2sub  11111  bernneq  11119  expnlbnd  11123  zzlesq  11167  faccl  11195  facdiv  11198  bcpasc  11226  bccl  11227  ffz0hash  11298  fnfzo0hash  11300  hashfibclem  11304  hashf1lem2  11308  wrdlen1  11364  wrdred1  11369  ccatval21sw  11395  wrdl1exs1  11419  ccatws1cl  11422  ccatws1leng  11424  pfxmpt  11474  pfxfv  11478  pfxfvlsw  11489  ccatpfx  11495  pfx1  11497  swrdccatin1  11519  swrdccat  11529  pfxccatpfx1  11530  2shfti  11618  crim  11645  mulreap  11651  resub  11657  imsub  11665  ipcnval  11673  cjsub  11679  resqrexlemfp1  11797  resqrexlemgt0  11808  sqabsadd  11843  sqabssub  11844  abs2dif2  11896  cau3lem  11903  icodiamlt  11969  xrmaxaddlem  12051  clim  12072  clim2  12074  clim2c  12075  clim0c  12077  2clim  12092  climabs0  12098  climcn1  12099  climcn2  12100  climsqz  12126  climsqz2  12127  climub  12135  climserle  12136  fsum3cvg  12170  fisumss  12184  fsum3ser  12189  sumsplitdc  12224  fsump1i  12225  fsumlessfi  12252  telfsumo  12258  fsumparts  12262  iserabs  12267  binomlem  12275  isumsplit  12283  isum1p  12284  isumlessdc  12288  mertenslem2  12328  mertensabs  12329  prodfap0  12337  prodfrecap  12338  prodfdivap  12339  fproddccvg  12364  prodmodclem2  12369  fprodssdc  12382  fprodabs  12408  fprodeq0  12409  fprodeq0g  12430  ege2le3  12463  efsub  12473  efexp  12474  efsep  12483  sinsub  12532  cossub  12533  demoivre  12565  eirraplem  12569  moddvds  12591  0dvds  12603  iddvdsexp  12607  dvdssub  12630  dvdsle  12636  dvdsleabs  12637  dvdseq  12640  dvdsflip  12643  mulsucdiv2z  12677  divalgb  12717  divalg2  12718  ndvdsadd  12723  bitsp1  12743  gcdneg  12784  gcdabs2  12792  modgcd  12793  bezoutlemsup  12811  gcdmultiplez  12823  gcdeq  12825  dvdssq  12833  lcmcllem  12870  lcmneg  12877  lcmdvds  12882  qredeu  12900  cncongrcoprm  12909  isprm3  12921  prmrp  12949  divnumden  13001  phiprmpw  13029  crth  13031  hashgcdlem  13045  hashgcdeq  13047  modprminv  13057  modprminveq  13058  modprmn0modprm0  13064  coprimeprodsq2  13066  pcpre1  13100  pccl  13107  pcmul  13109  pcdiv  13110  pcqcl  13114  pcexp  13117  pcdvds  13123  pcndvds  13125  pcndvds2  13127  pcelnn  13129  pcgcd1  13136  pc2dvds  13138  pc11  13139  gzsubcl  13188  4sqlem3  13198  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilemfrceq  13330  setsresg  13448  xpsfeq  13725  submcl  13845  grpinvnzcl  13936  mulgnnass  14019  nmzsubg  14072  nmznsg  14075  resghm2b  14124  ghmnsgpreima  14131  gzsumsnfd  14237  gsumunsnfd  14259  gsumresfi  14263  pwssnf1o  14318  iscrng2  14426  subrngpropd  14633  issubrg3  14664  subrgpropd  14670  islmodd  14738  lss1d  14829  lspsncl  14838  lspsnid  14853  df2idl2  14955  2idlcpbl  14970  qusrhm  14974  psrlidmfi  15199  psrridmfi  15200  iunopn  15228  unopn  15231  eltg  15278  eltg2  15279  tgcl  15290  tgiun  15299  tgidm  15300  isopn3i  15361  isneip  15372  neipsm  15380  restbasg  15394  restopn2  15409  lmbrf  15441  cnclima  15449  lmss  15472  txbasval  15493  txlm  15505  psmetxrge0  15558  blininf  15650  blssps  15653  blss  15654  elmopn2  15675  bdmet  15728  metrest  15732  bl2ioo  15776  dvcjbr  15934  plyaddlem1  15973  plymullem1  15974  plyreres  15990  dvply1  15991  dvply2g  15992  efper  16034  sinperlem  16035  abssinper  16073  cxpexprp  16128  logcxp  16130  rpcxpcl  16136  rpcxproot  16147  rprelogbmulexp  16192  log2tlbndlog2  16220  prmorcht  16282  bposlem2  16312  bpos  16320  lgsval2lem  16334  lgssq2  16365  lgsprme0  16366  ausgrusgrben  16614  wlkepvtx  16821  bj-inex  17138  peano5set  17171  findset  17176  bj-findis  17210  idjudju  17252  nninfsellemsuc  17261  nninfself  17262  cvgcmp2nlemabs  17287  iooref1o  17289  trilpolemeq1  17296  nconstwlpolemgt0  17321