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  6571  tfrlem9  6595  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  tfri3  6643  rdgtfr  6650  rdgruledefgg  6651  oav2  6741  oasuc  6742  omv2  6743  onasuc  6744  omsuc  6750  onmsuc  6751  nnaass  6763  nndi  6764  nndir  6768  nnaword  6789  ecelqsg  6867  iinerm  6886  ecovass  6923  ecoviass  6924  ecovdi  6925  ecovidi  6926  fvdiagfn  6981  ixpssmap2g  7015  domentr  7084  xpdom1g  7137  fopwdom  7142  ssenen  7158  phplem3  7161  phplem4  7162  php5dom  7170  ssfilem  7183  ssfilemd  7185  diffitest  7197  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  9693  zsubcl  9694  zltnle  9699  zrevaddcl  9704  nzadd  9706  zleltp1  9709  zltlem1  9711  zdiv  9744  peano2uz2  9763  uzind  9767  eluzp1l  9962  ublbneg  10028  qaddcl  10050  qsubcl  10053  qreccl  10057  qdivcl  10058  qrevaddcl  10059  irradd  10061  irrmul  10063  rerpdivcl  10101  nn0ledivnn  10184  xrre  10238  rexsub  10271  xaddass  10287  xnpcan  10290  xsubge0  10299  xposdif  10300  elioc2  10354  icoshft  10408  iccdil  10416  fzss2  10486  fzsuc2  10502  fzrev2  10508  elfzm11  10514  elfzp1b  10520  fzrevral  10528  fzshftral  10531  fzof  10567  fzoval  10571  fzon  10590  elfzoextl  10625  fzosubel  10628  zpnn0elfzo  10641  elfzom1b  10663  qltnle  10694  flapcl  10727  flaplelt  10729  flqlt  10737  flqbi  10745  flqaddz  10752  fzofig  10889  seq3feq2  10933  ser3le  10994  expp1  11003  expm1t  11024  expeq0  11027  binom2sub  11110  bernneq  11118  expnlbnd  11122  zzlesq  11166  faccl  11194  facdiv  11197  bcpasc  11225  bccl  11226  ffz0hash  11297  fnfzo0hash  11299  hashfibclem  11303  hashf1lem2  11307  wrdlen1  11363  wrdred1  11368  ccatval21sw  11394  wrdl1exs1  11418  ccatws1cl  11421  ccatws1leng  11423  pfxmpt  11473  pfxfv  11477  pfxfvlsw  11488  ccatpfx  11494  pfx1  11496  swrdccatin1  11518  swrdccat  11528  pfxccatpfx1  11529  2shfti  11617  crim  11644  mulreap  11650  resub  11656  imsub  11664  ipcnval  11672  cjsub  11678  resqrexlemfp1  11796  resqrexlemgt0  11807  sqabsadd  11842  sqabssub  11843  abs2dif2  11895  cau3lem  11902  icodiamlt  11968  xrmaxaddlem  12050  clim  12071  clim2  12073  clim2c  12074  clim0c  12076  2clim  12091  climabs0  12097  climcn1  12098  climcn2  12099  climsqz  12125  climsqz2  12126  climub  12134  climserle  12135  fsum3cvg  12169  fisumss  12183  fsum3ser  12188  sumsplitdc  12223  fsump1i  12224  fsumlessfi  12251  telfsumo  12257  fsumparts  12261  iserabs  12266  binomlem  12274  isumsplit  12282  isum1p  12283  isumlessdc  12287  mertenslem2  12327  mertensabs  12328  prodfap0  12336  prodfrecap  12337  prodfdivap  12338  fproddccvg  12363  prodmodclem2  12368  fprodssdc  12381  fprodabs  12407  fprodeq0  12408  fprodeq0g  12429  ege2le3  12462  efsub  12472  efexp  12473  efsep  12482  sinsub  12531  cossub  12532  demoivre  12564  eirraplem  12568  moddvds  12590  0dvds  12602  iddvdsexp  12606  dvdssub  12629  dvdsle  12635  dvdsleabs  12636  dvdseq  12639  dvdsflip  12642  mulsucdiv2z  12676  divalgb  12716  divalg2  12717  ndvdsadd  12722  bitsp1  12742  gcdneg  12783  gcdabs2  12791  modgcd  12792  bezoutlemsup  12810  gcdmultiplez  12822  gcdeq  12824  dvdssq  12832  lcmcllem  12869  lcmneg  12876  lcmdvds  12881  qredeu  12899  cncongrcoprm  12908  isprm3  12920  prmrp  12948  divnumden  13000  phiprmpw  13028  crth  13030  hashgcdlem  13044  hashgcdeq  13046  modprminv  13056  modprminveq  13057  modprmn0modprm0  13063  coprimeprodsq2  13065  pcpre1  13099  pccl  13106  pcmul  13108  pcdiv  13109  pcqcl  13113  pcexp  13116  pcdvds  13122  pcndvds  13124  pcndvds2  13126  pcelnn  13128  pcgcd1  13135  pc2dvds  13137  pc11  13138  gzsubcl  13187  4sqlem3  13197  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemodife  13297  ballotfilemfrceq  13329  setsresg  13447  xpsfeq  13724  submcl  13844  grpinvnzcl  13935  mulgnnass  14018  nmzsubg  14071  nmznsg  14074  resghm2b  14123  ghmnsgpreima  14130  gzsumsnfd  14236  gsumunsnfd  14258  gsumresfi  14262  pwssnf1o  14317  iscrng2  14425  subrngpropd  14632  issubrg3  14663  subrgpropd  14669  islmodd  14737  lss1d  14828  lspsncl  14837  lspsnid  14852  df2idl2  14954  2idlcpbl  14969  qusrhm  14973  psrlidmfi  15208  psrridmfi  15209  iunopn  15245  unopn  15248  eltg  15295  eltg2  15296  tgcl  15307  tgiun  15316  tgidm  15317  isopn3i  15378  isneip  15389  neipsm  15397  restbasg  15411  restopn2  15426  lmbrf  15458  cnclima  15466  lmss  15489  txbasval  15510  txlm  15522  psmetxrge0  15575  blininf  15667  blssps  15670  blss  15671  elmopn2  15692  bdmet  15745  metrest  15749  bl2ioo  15793  dvcjbr  15951  plyaddlem1  15990  plymullem1  15991  plyreres  16007  dvply1  16008  dvply2g  16009  efper  16051  sinperlem  16052  abssinper  16090  cxpexprp  16145  logcxp  16147  rpcxpcl  16153  rpcxproot  16164  rprelogbmulexp  16209  log2tlbndlog2  16237  prmorcht  16299  bposlem2  16329  bpos  16337  lgsval2lem  16351  lgssq2  16382  lgsprme0  16383  ausgrusgrben  16631  wlkepvtx  16838  bj-inex  17155  peano5set  17188  findset  17193  bj-findis  17227  idjudju  17269  nninfsellemsuc  17278  nninfself  17279  cvgcmp2nlemabs  17304  iooref1o  17306  trilpolemeq1  17313  nconstwlpolemgt0  17338