MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl12anc Structured version   Visualization version   GIF version

Theorem syl12anc 1321
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl12anc.4 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
syl12anc (𝜑𝜏)

Proof of Theorem syl12anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 3jca32 557 . 2 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
5 syl12anc.4 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
64, 5syl 17 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  syl22anc  1324  raaan  4054  soltmin  5491  xpdifid  5521  f1dom3fv3dif  6479  f1prex  6493  cocan1  6500  fliftfun  6516  soisores  6531  soisoi  6532  isopolem  6549  f1oiso2  6556  weniso  6558  caovcld  6780  caovcomd  6783  onminex  6954  tfrlem12  7430  omeulem1  7607  oaabs2  7670  omabs  7672  erov  7789  findcard2d  8146  frfi  8149  finsschain  8217  suplub2  8311  supgtoreq  8320  supisolem  8323  ordiso2  8364  ordtypelem7  8373  wemaplem2  8396  wemapsolem  8399  cantnflt  8513  cantnfp1lem3  8521  cantnflem1b  8527  cantnflem1  8530  wemapwe  8538  cnfcomlem  8540  cnfcom  8541  cnfcom3lem  8544  infxpenlem  8780  fseqenlem1  8791  dfac12lem2  8910  infpssrlem4  9072  enfin2i  9087  isf34lem7  9145  isf34lem6  9146  fin1a2lem7  9172  fin1a2lem10  9175  fin1a2lem11  9176  fin1a2lem13  9178  ttukeylem6  9280  ttukeylem7  9281  iundom2g  9306  fpwwe2lem6  9401  fpwwe2lem7  9402  fpwwe2lem9  9404  fpwwe2lem12  9407  fpwwe2  9409  canthnumlem  9414  canthwelem  9416  canthp1lem2  9419  pwfseqlem4  9428  inar1  9541  intgru  9580  distrlem4pr  9792  conjmul  10686  lediv12a  10860  recp1lt1  10865  cju  10960  gtndiv  11398  zsupss  11721  uzsupss  11724  icc0  12165  iccssioo2  12188  fzrev3  12348  elfz1b  12351  ico01fl0  12560  fldiv  12599  modabs  12643  modltm1p1mod  12662  modifeq2int  12672  seqcaopr  12778  seqf1olem1  12780  seqof2  12799  crreczi  12929  seqcoll  13186  seqcoll2  13187  hashtpg  13205  swrdccat3b  13433  sqrlem2  13918  resqrex  13925  abs1m  14009  isercoll  14332  zsum  14382  fsum2dlem  14429  fsumcom2  14433  fsumcom2OLD  14434  fprod2dlem  14635  fprodcom2  14639  fprodcom2OLD  14640  efsub  14755  bitsinv2  15089  sqgcd  15202  qredeu  15296  isprm7  15344  pcpremul  15472  pceulem  15474  pczpre  15476  pcdiv  15481  pcqmul  15482  pcqdiv  15486  pcexp  15488  pcdvdsb  15497  pcneg  15502  pcdvdstr  15504  pcgcd1  15505  pc2dvds  15507  pcz  15509  pcaddlem  15516  pcadd  15517  qexpz  15529  expnprm  15530  infpnlem2  15539  ramub2  15642  ramub1lem1  15654  setsstruct2  15817  f1ocpbllem  16105  f1ovscpbl  16107  mreexexlem3d  16227  mreexexlem4d  16228  fthi  16499  ipodrsima  17086  mndpropd  17237  grpsubpropd2  17442  ghmf1  17610  symgfvne  17729  f1omvdmvd  17784  f1otrspeq  17788  pmtrdifwrdel  17826  pmtrdifwrdel2  17827  psgnunilem2  17836  psgnunilem3  17837  psgnvalii  17850  odf1  17900  lsmpropd  18011  ablnnncan  18149  gsummptshft  18257  dprdf1o  18352  pgpfac1lem3  18397  pgpfac1lem5  18399  pgpfaclem1  18401  ablfaclem2  18406  srgbinomlem3  18463  ringpropd  18503  f1rhm0to0  18661  lmodprop2d  18846  lsspropd  18936  lmhmpropd  18992  lbspropd  19018  lbsextlem3  19079  assapropd  19246  psrass1  19324  psrass23l  19327  psrass23  19329  mplsubrg  19359  mplmon  19382  mplmonmul  19383  mplcoe1  19384  mplbas2  19389  mplind  19421  evlslem2  19431  mpfind  19455  gsumply1subr  19523  psrplusgpropd  19525  ply1scln0  19580  iporthcom  19899  obslbs  19993  scmataddcl  20241  scmatsubcl  20242  scmatmulcl  20243  smatvscl  20249  scmatrhmcl  20253  mat1scmat  20264  smadiadetglem2  20397  cramerimplem2  20409  cramerimplem3  20410  cramerimp  20411  1pmatscmul  20426  mat2pmatf1  20453  pm2mp  20549  chmatcl  20552  chmatval  20553  chmaidscmat  20572  chfacfisf  20578  cayhamlem1  20590  cpmidgsumm2pm  20593  cpmidpmat  20597  cpmadugsumfi  20601  cpmadumatpoly  20607  cayhamlem3  20611  pptbas  20722  elcls  20787  neiint  20818  neiptopnei  20846  restbas  20872  neitr  20894  iscnp4  20977  cnconst2  20997  cnpdis  21007  cnt0  21060  cnhaus  21068  cmpcovf  21104  hauscmplem  21119  conncompid  21144  2ndci  21161  2ndc1stc  21164  1stcrest  21166  2ndcctbss  21168  2ndcomap  21171  2ndcsep  21172  dis2ndc  21173  restlly  21196  islly2  21197  lly1stc  21209  dislly  21210  finlocfin  21233  dissnlocfin  21242  locfindis  21243  llycmpkgen2  21263  ptbasfi  21294  neitx  21320  ptpjopn  21325  ptcnplem  21334  upxp  21336  txlly  21349  txtube  21353  tx1stc  21363  txkgen  21365  xkococnlem  21372  kqreglem1  21454  kqreglem2  21455  kqnrmlem1  21456  kqnrmlem2  21457  hmeoimaf1o  21483  reghmph  21506  nrmhmph  21507  ordthmeolem  21514  trfil2  21601  fmfnfm  21672  hauspwpwf1  21701  fclsfnflim  21741  cnextf  21780  cnextcn  21781  tmdgsum2  21810  symgtgp  21815  subgntr  21820  opnsubg  21821  ghmcnp  21828  qustgpopn  21833  tsmsf1o  21858  tsmsxplem1  21866  tsmsxplem2  21867  tsmsxp  21868  ustexsym  21929  restutop  21951  imasdsf1olem  22088  blssexps  22141  blssex  22142  ssblex  22143  imasf1oxms  22204  blcld  22220  stdbdmopn  22233  met1stc  22236  met2ndci  22237  prdsxmslem2  22244  metcnp3  22255  cfilucfil  22274  ngptgp  22350  tgioo  22507  tgqioo  22511  zdis  22527  iccpnfhmeo  22652  xrhmeo  22653  cnheibor  22662  elpi1i  22754  cmetcusp  23058  pjthlem2  23117  ivthlem2  23128  ovolicc1  23191  ovolicc2lem3  23194  ovolicc2lem4  23195  volsup  23231  volivth  23281  vitalilem3  23285  mbflimsup  23339  mbfi1fseqlem1  23388  mbfi1fseqlem3  23390  mbfi1fseqlem5  23392  limcnlp  23548  limcflf  23551  limciun  23564  dvmptfsum  23642  dvcnvlem  23643  dvcvx  23687  facth1  23828  elply2  23856  plypf1  23872  coeeq  23887  aaliou3lem8  24004  ulm2  24043  mtestbdd  24063  reeff1o  24105  dcubic2  24471  quart  24488  xrlimcnp  24595  amgm  24617  harmonicbnd4  24637  perfect  24856  dchrptlem1  24889  bposlem2  24910  lgsfcl2  24928  lgsdir  24957  lgsdi  24959  lgsne0  24960  2lgslem1a1  25014  dchrvmasumlem2  25087  chpdifbndlem2  25143  pntpbnd1  25175  pntpbnd2  25176  padicabv  25219  tgcgrxfr  25313  idmot  25332  legid  25382  btwnleg  25383  leg0  25387  tghilberti1  25432  mirreu3  25449  colperpex  25525  lnopp2hpgb  25555  axcgrrflx  25694  axsegconlem1  25697  axcontlem2  25745  axcontlem12  25755  eengtrkg  25765  wwlksnredwwlkn  26659  clwwlksel  26780  clwlksfclwwlk  26828  0wlkon  26847  0trlon  26851  upgr3v3e3cycl  26906  numclwwlkovf2ex  27075  frgrogt3nreg  27109  nvpi  27371  nmlno0lem  27497  fh1  28326  fh2  28327  eigposi  28544  nmlnop0iALT  28703  nmopun  28722  branmfn  28813  opsqrlem1  28848  opsqrlem6  28853  mdslmd1lem1  29033  csmdsymi  29042  atom1d  29061  chirredlem2  29099  cdj1i  29141  cdj3i  29149  fcnvgreu  29315  xrofsup  29377  2sqmod  29433  archirngz  29528  archiabllem2a  29533  gsummpt2d  29566  orngsqr  29589  ornglmullt  29592  orngrmullt  29593  metideq  29718  metider  29719  pstmfval  29721  lmxrge0  29780  qqhval2  29808  qqhf  29812  qqhghm  29814  qqhrhm  29815  esumpcvgval  29921  esum2dlem  29935  esum2d  29936  sigainb  29980  insiga  29981  ddemeas  30080  imambfm  30105  dya2icoseg  30120  dya2iocnrect  30124  eulerpartlemgvv  30219  probun  30262  ballotlemfc0  30335  ballotlemfcc  30336  sgnmul  30385  signstfvneq0  30429  erdszelem8  30888  erdszelem9  30889  erdsze2lem2  30894  cnpconn  30920  txpconn  30922  ptpconn  30923  indispconn  30924  connpconn  30925  cvxpconn  30932  cnllysconn  30935  cvmcov2  30965  cvmopnlem  30968  cvmliftmolem1  30971  cvmliftlem14  30987  cvmliftlem15  30988  cvmlift2lem13  31005  cvmlift3lem2  31010  cvmlift3lem9  31017  poseq  31451  sltres  31518  nodense  31552  nocvxmin  31554  nobndup  31563  nobnddown  31564  noprefixmo  31573  seglerflx  31861  seglemin  31862  btwnsegle  31866  hilbert1.1  31903  neibastop2lem  31997  bj-finsumval0  32780  relowlssretop  32843  wl-2sb6d  32973  tan2h  33033  poimirlem1  33042  poimirlem3  33044  poimirlem4  33045  poimirlem9  33050  poimirlem22  33063  poimirlem28  33069  heicant  33076  mblfinlem2  33079  itg2addnc  33096  ftc2nc  33126  dvasin  33128  sdclem1  33171  fdc  33173  istotbnd3  33202  sstotbnd  33206  prdstotbnd  33225  prdsbnd2  33226  cntotbnd  33227  rngoisocnv  33412  lsmsat  33775  islfld  33829  ps-2  34244  lplnexllnN  34330  4atlem9  34369  4atlem10a  34370  lnatexN  34545  2lnat  34550  pmapjat1  34619  lhpj1  34788  lhpm0atN  34795  4atexlemex2  34837  4atex  34842  4atex2-0aOLDN  34844  4atex2-0cOLDN  34846  lautcnvle  34855  lautj  34859  lautm  34860  idltrn  34916  cdleme01N  34988  cdleme0ex1N  34990  cdleme5  35007  cdleme9  35020  cdleme11c  35028  cdleme11g  35032  cdlemefrs29bpre0  35164  cdlemefrs29cpre1  35166  cdlemefrs32fva1  35169  cdleme32fva  35205  cdleme32fva1  35206  cdleme32fvaw  35207  cdleme32d  35212  cdleme32f  35214  cdleme35fnpq  35217  cdleme48d  35303  cdleme48gfv  35305  cdleme50ltrn  35325  trlord  35337  cdlemg4b1  35377  cdlemg4b2  35378  cdlemg13a  35419  cdlemg17a  35429  cdlemg17f  35434  erng1lem  35755  erngdvlem3  35758  erngdvlem4  35759  erng1r  35763  erngdvlem3-rN  35766  erngdvlem4-rN  35767  dva0g  35796  dialss  35815  dia0  35821  dia1N  35822  diaglbN  35824  diameetN  35825  diainN  35826  diaintclN  35827  dia1dim  35830  dia2dimlem5  35837  dia2dimlem7  35839  dia2dimlem9  35841  dia2dimlem10  35842  dia2dimlem12  35844  dia2dimlem13  35845  dvhopvadd  35862  dvhvaddass  35866  dvhopvsca  35871  tendolinv  35874  tendorinv  35875  dvhlveclem  35877  dvh0g  35880  dvheveccl  35881  dvhopN  35885  docaclN  35893  diaocN  35894  djajN  35906  dib0  35933  dib1dim  35934  dibglbN  35935  dibintclN  35936  dib1dim2  35937  diblss  35939  diblsmopel  35940  dicvaddcl  35959  dicvscacl  35960  diclspsn  35963  cdlemn4a  35968  cdlemn11c  35978  dihjustlem  35985  dihord1  35987  dihord2a  35988  dihord2b  35989  dihord2cN  35990  dihord11b  35991  dihord11c  35993  dihord2pre  35994  dihlsscpre  36003  dih1dimb  36009  dib2dim  36012  dih2dimb  36013  dih2dimbALTN  36014  dihvalcq2  36016  dihopelvalcpre  36017  dihord6apre  36025  dihord5b  36028  dihord5apre  36031  dih0  36049  dihmeetlem1N  36059  dihglblem5apreN  36060  dihglblem3N  36064  dihmeetlem2N  36068  dihglbcpreN  36069  dihmeetlem4preN  36075  dih1dimatlem0  36097  dih1dimatlem  36098  dihatlat  36103  dihatexv  36107  dihglb2  36111  dihmeet  36112  dihintcl  36113  dihmeet2  36115  doch2val2  36133  dochocss  36135  dihoml4c  36145  dochdmj1  36159  djhlj  36170  djhljjN  36171  djhjlj  36172  dihsumssj  36177  djhexmid  36180  djhlsmcl  36183  djhcvat42  36184  dihjatcclem4  36190  dihjat1lem  36197  dihsmsprn  36199  dihjat3  36201  dvh3dim2  36217  dvh3dim3N  36218  dochkr1OLDN  36248  lclkrlem2c  36278  lclkrlem2d  36279  mapdpglem23  36463  hdmap11lem2  36614  mzpcompact2lem  36794  diophrw  36802  rexrabdioph  36838  eldioph4b  36855  pellexlem5  36877  pellfund14  36942  acongtr  37025  fnwe2lem3  37102  gicabl  37149  hbtlem2  37175  hbtlem4  37177  hbtlem5  37179  dgraalem  37196  aaitgo  37213  ioounsn  37276  ntrclsk13  37851  gneispb  37911  wessf1ornlem  38845  ltdiv23neg  39081  islptre  39255  limclner  39287  icccncfext  39404  stoweidlem1  39525  stoweidlem14  39538  stoweidlem24  39548  stoweidlem46  39570  stoweidlem57  39581  dirkercncflem2  39628  fourierdlem20  39651  fourierdlem41  39672  fourierdlem46  39676  fourierdlem48  39678  fourierdlem50  39680  fourierdlem62  39692  fourierdlem63  39693  fourierdlem64  39694  fourierdlem65  39695  fourierdlem76  39706  fourierdlem79  39709  fourierdlem103  39733  fourierdlem104  39734  etransclem47  39805  raaan2  40479  iccpartiun  40668  sqrtpwpw2p  40749  fmtnoprmfac1lem  40775  fmtnoprmfac2lem1  40777  lighneallem4a  40824  perfectALTV  40927  nnsum4primeseven  40977  nnsum4primesevenALTV  40978  mgmpropd  41063  lidlmmgm  41213  gsumlsscl  41452  lincsumcl  41508  lincscmcl  41509  isldepslvec2  41562  m1modmmod  41604  elbigo2  41638  relogbdivb  41648  blennnt2  41675  dignn0ldlem  41688
  Copyright terms: Public domain W3C validator