Theorem syl2an 454

Description: A double syllogism inference.

Hypotheses

Ref	Expression
sylan.1	⊢ ((φ ⋀ ψ) → χ)
syl2an.2	⊢ (θ → φ)
syl2an.3	⊢ (τ → ψ)

Assertion

Ref	Expression
syl2an	⊢ ((θ ⋀ τ) → χ)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		sylan.1	. . 3 ⊢ ((φ ⋀ ψ) → χ)
2		syl2an.2	. . 3 ⊢ (θ → φ)
3	1, 2	sylan 448	. 2 ⊢ ((θ ⋀ ψ) → χ)
4		syl2an.3	. 2 ⊢ (τ → ψ)
5	3, 4	sylan2 451	1 ⊢ ((θ ⋀ τ) → χ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  ax11indalem 1366  sbccomg 1985  csbcomg 2013  csbnestg 2032  ssconb 2166  ineqan12d 2215  ifpr 2423  breqan12d 2627  copsex2g 2788  unexg 2869  tz7.7 2968  ordin 2972  onin 2973  ontri1 2976  ordon 2982  onelpsst 2993  onsseleq 2994  ontr2 2999  peano4 3147  findsg 3152  vtoclr 3206  opthprc 3216  ssxp 3251  relop 3270  sotri 3435  unixp 3509  coexg 3516  funsn 3535  funco 3542  funssres 3544  fnco 3587  fco 3627  fodmrnu 3671  eqfnfv 3788  fconst2g 3836  isofrlem 3892  tfrlem5 3906  tfrlem11 3912  tz7.48lem 3946  opreqan12d 3970  oprabval5 4020  curry1 4088  oacan 4172  oawordri 4174  oaass 4185  omord2 4188  omcan 4190  oeord 4205  oecan 4206  oeordsuc 4211  nnasuc 4215  nnmsuc 4216  nnecl 4221  nnacom 4223  nnaordi 4224  nnaword1 4234  nnmordi 4236  oaabslem 4241  oaabs 4242  omsmo 4247  brecop 4296  ecopoprtrn 4301  th3qlem1 4304  ecoprdi 4311  mapvalg 4320  pmvalg 4321  mapsn 4335  en2sn 4418  sbthlem7 4439  sbth 4443  sdomnsym 4448  xpen 4474  mapenlem1 4475  mapenlem2 4476  mapdom1 4478  mapdom2 4480  limenpsi 4491  phplem4 4497  php 4499  php3 4501  nndomo 4506  ominf 4514  pssnn 4519  unblem2 4524  isfinite2 4529  unfilem1 4530  unfilem2 4531  unfi2 4535  unifi2 4539  fodomfi 4546  inf3lem6 4598  rankxplim 4692  aceq5lem4 4718  kmlem6 4750  zorn2lem6 4773  fodom 4778  brdom6disj 4785  cardnn 4804  carddomi 4815  unxpdomlem 4823  unxpdom2 4825  ondomcard 4837  cdavalt 4899  cdafi 4916  axrepndlem2 4925  axrepnd 4926  ltsopi 4996  mulclpi 5001  addcompi 5002  mulcompi 5004  distrpi 5006  ltexpi 5009  ltapi 5010  ltmpi 5011  addcmpblnq 5032  mulpipq 5035  addclpq 5038  addasspq 5043  distrpq 5047  ltsopq 5055  ltrpq 5065  genpnnp 5088  mulclprlem 5101  distrlem1pr 5107  distrlem5pr 5111  addcanpr 5132  reclem3pr 5138  mulcmpblnr 5163  addsrpr 5164  mulclsr 5173  mulasssr 5179  distrsr 5180  ltsosr 5183  1idsr 5187  00sr 5188  recexsrlem 5192  mulgt0sr 5194  suppsr3 5204  addcnsr 5233  axmulopr 5246  axmulass 5258  axdistr 5259  ax0id 5261  axcnre 5266  cnegextlem3 5327  cnegext 5328  muladdt 5401  resubclt 5418  addsub4t 5453  mulsubt 5457  ltxrltt 5480  axltadd 5485  lenltt 5490  ltadd2t 5606  leadd2t 5608  ltsubadd2t 5610  lesubadd2t 5612  ltaddsub2t 5614  leaddsub2t 5616  addgtge0t 5630  ltaddpos2t 5633  posdift 5635  addge02t 5654  subge0t 5655  suble0t 5656  recextlem1 5663  recextlem2 5664  recext 5665  divmuldivt 5744  divdivdivt 5749  conjmult 5761  prodgt02t 5791  prodge02t 5793  lemul2t 5797  lemul1it 5801  lemul1itOLD 5802  lemul2it 5803  lemul2itOLD 5804  ltmulgt12t 5811  ltmuldiv2t 5826  ltdivmult 5827  ledivmult 5828  ltdivmul2t 5829  lt2mul2divt 5830  ledivmul2t 5831  lemuldiv2t 5833  lerec 5836  ledivdivt 5846  lediv2t 5847  max1 5871  max2 5873  min1 5875  min2 5876  nnaddclt 5896  nnmulclt 5897  nnleltp1t 5909  nnltp1let 5910  nnaddm1clt 5913  nndivt 5914  reuunineg 6021  nnreclt 6027  supxrbnd1 6050  supxrbnd2 6051  nn0nnaddclt 6081  nn0leltp1t 6083  nn0ltlem1t 6084  nn0subt 6116  zaddclt 6120  zsubclt 6123  znnsubt 6132  znn0subt 6133  zmulclt 6135  zleltp1t 6137  nn0lem1ltt 6140  nnlem1ltt 6141  nnltlem1t 6142  z2get 6143  zextlet 6144  zextltt 6145  btwnnzt 6147  primet 6150  zneo 6155  zneoOLD 6156  peano2uz2 6157  uzind 6161  uzindOLD 6164  uzwo4OLD 6166  zmax 6176  rebtwnz 6178  flget 6186  flltt 6187  flval3t 6190  fladdzt 6195  qret 6205  qnegclt 6216  qsubclt 6218  qrecclt 6219  qbtwnre 6224  qbtwnxr 6225  rpaddclt 6235  rpmulclt 6236  rpdivclt 6237  monoord 6239  om2uzlt 6243  om2uzlt2 6244  om2uzf1o 6246  ser1add2 6283  ser1add 6284  elioc2t 6330  elico2t 6331  elicc2t 6332  ioonegt 6347  icoshftf1oi 6350  snunioolem 6355  uznegit 6369  uz11t 6372  eluzp1m1t 6373  eluzp1p1t 6375  uzaddclt 6389  uzwo 6395  uzwoOLD 6396  indstr 6401  elfz1eqt 6432  fznt 6433  elfz2nn0t 6435  fznn0sub2t 6439  fzaddelt 6440  fzsubelt 6441  fzoptht 6442  fzrev2t 6452  fzrev3t 6454  fzrevralt 6459  fzrevral3t 6461  fzshftralt 6462  fseqsupcl 6465  seqzp1 6488  seqzval2t 6493  seqzrn2 6496  expp1t 6514  expcllem 6515  expaddt 6535  expmult 6536  expsubt 6537  expordit 6539  expcant 6540  expordt 6541  expwordit 6542  expmwordit 6545  lt2sqt 6569  le2sqt 6570  bernneq 6591  bernneq2 6592  expnbndt 6593  nn0opthlem2 6603  sqrlem6 6616  sqrlem12 6622  sqrle 6645  sqrlt 6646  sqr4 6655  sqr9 6656  sqr2irr 6667  crret 6710  crretOLD 6711  crimt 6712  crimtOLD 6713  resubt 6749  imsubt 6752  cjsubt 6759  cjreimt 6771  cjreim2t 6772  cj11t 6773  absreimsqt 6799  absreimt 6800  absdifltt 6829  absdiflet 6830  abssuble0t 6842  abs2difabst 6848  seq1bnd 6855  cau2 6858  cau4i 6863  cau5 6864  cvg1i 6865  cvg1 6866  cvg3 6868  caubnd 6871  caure 6872  cauim 6873  ser1absdiflem 6874  ser1absdif 6875  facdivt 6887  facwordit 6889  faclbnd 6890  faclbnd3 6892  faclbnd4lem4 6896  faclbnd5 6898  faclbnd6 6899  facavgt 6900  bcval4t 6907  bccmplt 6908  bccl2t 6917  fsum1ps 6964  fsumsplit 6966  fsumadd 6968  fsumrev 6975  fsumrev2 6976  fsumshft 6977  fsumshftm 6978  fsumcmp 6986  fsumcmpndx2 6988  fsumabs 6989  fsumabs2mul 6990  binomlem1 7012  binomlem2 7013  binomlem4 7015  binomlem5 7016  clm3 7025  climshft 7049  climge0 7057  climaddlem3 7060  climmullem1 7064  climmullem5 7068  climmullem8 7071  climsub 7074  clim2serzt 7078  clim2serz 7089  climserzle 7091  climcau 7100  caucvglem5 7105  caucvglem6 7106  caucvg 7107  serzf0 7113  ser1f0 7114  ser1cmp2lem 7120  ser1cmp2 7121  cvgcmp3c 7130  reccnv 7161  infcvglem1 7164  geoser 7177  cvgratlem2ALT 7191  cvgratlem1 7193  cvgratlem2 7194  fsum0diaglem2 7200  fsum0diag4 7204  negfcncf 7212  mulc1cncf 7222  ivthlem6 7229  ivthlem7 7230  ivthlem8 7231  ivthlem6OLD 7238  ivthlem7OLD 7239  efseq0ex 7261  efaddlem3 7290  efaddlem5 7292  efaddlem6 7293  efaddlem11 7298  efaddlem13 7300  efaddlem14 7301  efaddlem17 7304  efaddlem19 7306  abspef01tlub 7344  reeff1o 7376  efieq 7400  sinsubt 7405  cossubt 7406  subsint 7408  addcost 7409  subcost 7410  nn0ennn 7447  xpnnen 7449  znnenlem 7451  znnenlemOLD 7452  znnen 7453  infpnlem1 7457  infpn2 7460  infxpidmlem1 7503  infxpidmlem11 7513  infxpidmlem12 7514  infunabs 7516  infcdaabs 7517  infdif 7519  infxpabs 7521  infmap1 7524  iunctb 7525  unctb 7527  alephmul 7533  subbas 7594  subtop 7596  retopbas 7605  neiint 7669  innei 7686  islp2 7697  iscn 7708  iscnp 7710  cnco 7718  cnconst 7730  sncld 7737  metxplem1 7778  metxplem2 7779  metxp 7786  bl2in 7795  opnin 7821  metcnp 7839  metcn 7841  cncfmet 7857  remetdval 7860  bl2ioo 7863  ioo2bl 7864  blssioo 7865  tgioolem 7866  lmuni 7902  caussi 7905  causs 7906  lmle 7911  xplm 7925  xpcn 7926  bcthlem8 7956  bcthlem9 7957  bcthlem18 7966  bcthlem20 7968  bcthlem21 7969  resgrprnOLD 8046  abldivdiv4 8061  ablmul 8083  ghgrpilem1 8085  ghsubgi 8090  vcoprnelem 8149  sqcn 8283  nmcnilem 8285  sm1cnilem 8294  nvo00 8369  nmoge0 8375  nmorepnf 8376  nmolb 8379  nmoub3i 8381  blocnilem 8408  blocni 8409  cnph 8422  ipasslem1 8434  ipasslem2 8435  ipasslem4 8437  ipasslem8 8441  ipasslem11 8444  ipblnfi 8460  phoeqi 8462  ubthlem7 8479  ubthlem8 8480  ubthlem9 8481  ubthlem10 8482  ubthlem11 8483  ubthlem12 8484  ubthlem13 8485  ubthlem14 8486  minveclem9 8497  minveclem16 8504  minveclem18 8506  minveclem19 8507  minveclem21 8509  minveclem24 8512  minveclem25 8513  minveclem26 8514  minveclem27 8515  minveclem28 8516  minveclem30 8518  minveclem31 8519  minveclem36 8524  minveclem38 8526  minveceu 8527  htthlem6 8568  htthlem8 8570  pilem2 8610  pilem3 8611  pigt2lt4 8613  sincosq1sgn 8640  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  sincosq1eq 8645  sincos6thpi 8647  cosh111lem1 8648  efgh 8652  efifolem1 8656  efifolem2 8657  efifolem3 8658  efifolem4 8659  efifolem5 8660  efifolem6 8661  efifolem7 8662  efif1lem1 8664  efif1lem3 8666  efif1lem4 8667  circgrpOLD 8677  eff1i 8683  relogeftb 8704  relogoprlem 8708  relogexpt 8713  hvsub4t 8845  his7t 8895  his2sub2t 8898  hial2eq2t 8912  normpyct 8952  hhph 8984  bcs2t 8988  hcau2 8994  hhssabl 9071  hhssnv 9073  hhsscms 9089  ocorth 9103  chocuni 9111  projlem2 9126  projlem26 9150  projlem28 9152  projlem31 9155  pjtheu2 9188  pjpj0 9193  shsel3t 9217  shscl 9219  chsupss 9248  shjvalt 9259  chjvalt 9260  shjclt 9266  chjclt 9267  shsvs 9274  shslej 9276  chslejt 9359  chjcomt 9367  chub1t 9368  chdmj1t 9390  spanunsn 9442  spanpr 9443  fh1t 9501  fh2t 9502  cm2jt 9503  osumlem2 9519  osumlem3 9520  spansncv 9537  5oalem1 9539  5oalem3 9541  5oalem5 9543  3oalem2 9548  pjv 9590  pjds3 9598  hoaddclt 9624  hoeqt 9626  hoadddit 9669  hoadddirt 9670  hosubdit 9674  hosub4t 9679  hoeq1t 9696  hoeq2t 9697  counopt 9784  adjeqt 9798  brafnmult 9814  lnopsub 9837  hmopst 9883  hmopmt 9884  hmopdt 9885  hmopcot 9886  nmcopexlem1 9889  nmcopexlem3 9891  nmcopexlem5 9893  nmcopexlem6 9894  lnopcon 9901  lnfnsub 9913  nmcfnexlem1 9918  nmcfnexlem3 9920  nmcfnexlem5 9922  nmcfnexlem6 9923  lnfncon 9928  nlelsh 9931  riesz3 9933  riesz1t 9936  cnlnadjlem2 9939  cnlnadjlem6 9943  cnlnssadj 9951  adjlnopt 9957  adjmult 9963  adjaddt 9964  nmopco 9966  cnvbramult 9986  kbass2t 9988  kbass4t 9990  kbass6t 9992  leopaddt 10003  leopmul2it 10006  leoptrit 10007  leopnmidt 10009  hmopidmch 10017  cvcon3t 10149  dmdmdt 10165  mddmdt 10166  ssdmd1 10177  ssdmd2 10178  cvdmdt 10201  superpos 10218  chrelat 10228  atcv0eq 10243  atoml 10246  atcvatlem 10249  atcvat 10250  atcvat2 10251  irredlem4 10257  atcvat3 10260  atcvat4 10261  mdsymlem2 10268  mdsymlem3 10269  mdsymlem5 10271  mdsymlem8 10274  dmdsymt 10277  cdjreu 10293  cdj1 10294  cdj3lem2b 10298  cdj3lem3 10299  cdj3lem3b 10301  cdj3 10302  elghomlem1 10316  cayleylem2 10344  uninqs 10378  elo 10381  cdrci 10417  homeofval 10439  fgsb 10480  fgsb2 10485  dtt2 10498  dmse1 10503  trran 10516  cnvtr 10518  1ded 10551  1cat 10572  ismonc 10620

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain