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

Theorem syl22anc 1325
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl22anc.5 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
Assertion
Ref Expression
syl22anc (𝜑𝜂)

Proof of Theorem syl22anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
31, 2jca 554 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl22anc.5 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
73, 4, 5, 6syl12anc 1322 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:  preqsnd  4383  fr2nr  5082  soltmin  5520  f1oprg  6168  f1prex  6524  fveqf1o  6542  weniso  6589  fr3nr  6964  smogt  7449  smorndom  7450  oacomf1o  7630  difsnen  8027  undom  8033  enfixsn  8054  domss2  8104  ssenen  8119  marypha1lem  8324  fisupcl  8360  ordtypelem3  8410  ordtypelem8  8415  oieu  8429  oismo  8430  wofib  8435  wemaplem2  8437  wemapso  8441  wemapso2lem  8442  unxpwdom2  8478  infdifsn  8539  oemapvali  8566  cantnflem1c  8569  cantnflem1  8571  cantnf  8575  cnfcom3  8586  r1ordg  8626  dif1card  8818  infxpenlem  8821  dfac8clem  8840  infxp  9022  infmap2  9025  cflim2  9070  coftr  9080  fin2i2  9125  enfin2i  9128  fin23lem26  9132  fin23lem27  9135  fin23lem40  9158  isf32lem2  9161  isf32lem3  9162  isf32lem4  9163  isf32lem7  9166  isf32lem9  9168  fin1a2lem13  9219  fin12  9220  alephexp1  9386  gchdomtri  9436  fpwwe2lem12  9448  fpwwe2lem13  9449  gchpwdom  9477  gchhar  9486  adderpqlem  9761  mulerpqlem  9762  addassnq  9765  mulassnq  9766  distrnq  9768  mulidnq  9770  recmulnq  9771  ltexnq  9782  distrlem1pr  9832  distrlem4pr  9833  prlem936  9854  reclem3pr  9856  mulcmpblnr  9877  mulgt0d  10177  mul4d  10233  add4d  10249  add42d  10250  subcan  10321  addsub4d  10424  subadd4d  10425  sub4d  10426  2addsubd  10427  addsubeq4d  10428  muladdd  10474  mulsubd  10475  addgegt0d  10586  addge0d  10588  mulge0d  10589  le2addd  10631  le2subd  10632  ltleaddd  10633  leltaddd  10634  lt2subd  10636  divdivdiv  10711  divcan5  10712  divne0d  10802  recdivd  10803  recdiv2d  10804  divcan6d  10805  ddcand  10806  rec11d  10807  divmuldivd  10827  divmul13d  10828  divmul24d  10829  divadddivd  10830  divsubdivd  10831  divmuleqd  10832  divdivdivd  10833  subrecd  10841  mulge0b  10878  recreclt  10907  divgt0d  10944  mulgt1d  10945  lemulge11d  10946  lemulge12d  10947  ltmul12ad  10950  lemul12ad  10951  lemul12bd  10952  supmul1  10977  nndivtr  11047  qreccl  11793  ledivdivd  11882  lediv12ad  11916  lt2mul2divd  11924  xlt2add  12075  supxrun  12131  supxrre  12142  infxrre  12151  elicore  12211  iccss2  12229  iccssico2  12232  lincmb01cmp  12300  iccf1o  12301  fzrev2i  12390  fz1fzo0m1  12499  2tnp1ge0ge0  12613  m1modnnsub1  12699  modaddmodup  12716  modaddmodlo  12717  modsubdir  12722  fzennn  12750  sermono  12816  mulexpz  12883  expaddz  12887  ltexp2a  12895  leexp2a  12899  sqdiv  12911  expmulnbnd  12979  digit1  12981  expsubd  13002  lt2sqd  13026  le2sqd  13027  sq11d  13028  bcm1k  13085  bcp1n  13086  bcp1nk  13087  hashf1lem1  13222  cshw1  13549  2swrd2eqwrdeq  13677  ofccat  13689  absrele  14029  sqreulem  14080  sqrtmuld  14144  sqrtsq2d  14145  sqrtled  14146  sqrtltd  14147  sqr11d  14148  abs3lemd  14181  rlimuni  14262  climuni  14264  lo1resb  14276  o1resb  14278  2clim  14284  addcn2  14305  mulcn2  14307  o1of2  14324  o1rlimmul  14330  lo1add  14338  lo1mul  14339  isercolllem1  14376  caucvgrlem  14384  iseraltlem2  14394  iseraltlem3  14395  iseralt  14396  mptfzshft  14491  fsumrev  14492  fsum0diag2  14496  binomlem  14542  climcndslem1  14562  climcndslem2  14563  harmonic  14572  mertenslem1  14597  fprodser  14660  fprodrev  14688  rprisefaccl  14735  efcllem  14789  moddvds  14972  dvds1  15022  dvdsext  15024  oexpneg  15050  evennn02n  15055  evennn2n  15056  bitsinv1  15145  sadaddlem  15169  sadasslem  15173  sadeq  15175  mulgcd  15246  dvdssqlem  15260  lcmftp  15330  rpmulgcd2  15351  coprmproddvdslem  15357  isprm5  15400  isprm6  15407  crth  15464  eulerthlem2  15468  prmdiveq  15472  pythagtriplem11  15511  pythagtriplem13  15513  iserodd  15521  pcgcd1  15562  pcprmpw2  15567  pcaddlem  15573  fldivp1  15582  4sqlem12  15641  4sqlem14  15643  4sqlem15  15644  4sqlem16  15645  vdwapun  15659  mreexexlem4d  16288  acsfn1  16303  acsfn2  16305  sscpwex  16456  rescabs  16474  yonedainv  16902  subm0  17337  pmtrfb  17866  psgnunilem1  17894  odmodnn0  17940  odeq  17950  dfod2  17962  sylow1lem1  17994  lsmsubg  18050  lsmmod  18069  lsmdisj2  18076  ghmplusg  18230  odadd  18234  gexexlem  18236  lt6abl  18277  cyggex2  18279  dprdfinv  18399  dmdprdsplitlem  18417  dpjidcl  18438  ablfacrp  18446  ablfacrp2  18447  ablfac1c  18451  ablfac1eu  18453  lcomfsupp  18884  lssvancl1  18926  lssvnegcl  18937  lspprvacl  18980  lspsneli  18982  lspsn  18983  lmhmplusg  19025  lmhmima  19028  lmhmpreima  19029  reslmhm  19033  lbsind2  19062  lsmcl  19064  lsmelval2  19066  lsppreli  19071  lspprabs  19076  pj1lmhm  19081  lssvs0or  19091  lspabs3  19102  lspfixed  19109  lspexch  19110  lsmcv  19122  lspsolv  19124  lidlmcl  19198  drngnidl  19210  2idlcpbl  19215  mplbas2  19451  evlslem3  19495  evlslem1  19496  coe1addfv  19616  lply1binom  19657  evl1addd  19686  evl1subd  19687  evl1muld  19688  gzrngunit  19793  zringlpirlem3  19815  prmirredlem  19822  znf1o  19881  znunithash  19894  frlmsubgval  20089  frlmvscaval  20091  frlmphllem  20100  frlmphl  20101  frlmssuvc1  20114  frlmsslsp  20116  frlmup1  20118  frlmup2  20119  lindfind2  20138  lindfrn  20141  f1lindf  20142  islindf4  20158  mamudi  20190  mamudir  20191  1marepvmarrepid  20362  mdetrlin  20389  smadiadetglem1  20458  smadiadetg  20460  cramerimplem1  20470  mat2pmatscmxcl  20526  m2pmfzgsumcl  20534  pmatcollpw  20567  pmatcollpwfi  20568  pmatcollpw3fi1lem1  20572  cpmidpmatlem2  20657  cpmadugsumlemF  20662  chcoeffeqlem  20671  ntrin  20846  topssnei  20909  restbas  20943  restntr  20967  cnntri  21056  fiuncmp  21188  nllyrest  21270  nllyidm  21273  hausllycmp  21278  cldllycmp  21279  hauspwdom  21285  txcld  21387  txcn  21410  txlly  21420  txnlly  21421  txhaus  21431  txlm  21432  txkgen  21436  xkococnlem  21443  cnmpt2res  21461  xkoinjcn  21471  basqtop  21495  qtopeu  21500  trfbas2  21628  neifil  21665  hausflim  21766  alexsubALTlem2  21833  cnextfval  21847  cnextfvval  21850  cnextf  21851  cnextfres  21854  clssubg  21893  utop2nei  22035  utop3cls  22036  utopreg  22037  psmetlecl  22101  xmetlecl  22132  prdsxmetlem  22154  bldisj  22184  imasf1obl  22274  prdsbl  22277  stdbdmet  22302  stdbdmopn  22304  met2ndci  22308  metcnp  22327  metustto  22339  metustexhalf  22342  cfilucfil  22345  metucn  22357  lssnlm  22486  nmotri  22524  nmoid  22527  tgioo  22580  blcvx  22582  xrsmopn  22596  reperflem  22602  reconnlem2  22611  opnreen  22615  metdsge  22633  metdsre  22637  metdscnlem  22639  metnrmlem1a  22642  metnrmlem1  22643  metnrmlem3  22645  cncfmet  22692  cnmpt2pc  22708  icopnfcnv  22722  icopnfhmeo  22723  cnllycmp  22736  evth  22739  lebnumii  22746  nmoleub2lem3  22896  iscfil2  23045  cfil3i  23048  iscfil3  23052  cfilfcls  23053  iscau3  23057  iscmet3lem2  23071  caubl  23087  lmcau  23092  rrxcph  23161  minveclem2  23178  pjthlem1  23189  pjthlem2  23190  ivthicc  23208  ovollecl  23232  ovolunlem1a  23245  ovolunnul  23249  ovoliunlem1  23251  ismbl2  23276  nulmbl2  23285  unmbl  23286  volun  23294  voliunlem2  23300  ioombl1lem2  23308  uniioombllem2a  23331  uniioombllem3  23334  uniioombllem4  23335  dyaddisjlem  23344  dyadmaxlem  23346  opnmbllem  23350  volsup2  23354  volcn  23355  ismbfd  23388  mbfi1fseqlem1  23463  mbfi1fseqlem5  23467  itg2lecl  23486  itg2monolem2  23499  itg2gt0  23508  itgspliticc  23584  ellimc3  23624  limcres  23631  dvfval  23642  dvres3  23658  dvres3a  23659  dvnff  23667  dvnadd  23673  dvn2bss  23674  dvnres  23675  dvcmul  23688  dvcmulf  23689  dvmptres3  23700  dvmptres2  23706  dvmptntr  23715  dvexp3  23722  dvferm1lem  23728  dvlip  23737  dvlipcn  23738  dvlip2  23739  c1liplem1  23740  dvgt0lem1  23746  dvgt0lem2  23747  dvne0  23755  lhop1lem  23757  lhop2  23759  lhop  23760  dvcnvrelem1  23761  dvcnvrelem2  23762  dvcvx  23764  dvfsumle  23765  dvfsumabs  23767  dvfsumlem2  23771  ftc1lem6  23785  ftc1  23786  ftc2ditglem  23789  itgsubstlem  23792  tdeglem4  23801  mdegaddle  23815  mdegmullem  23819  ply1rem  23904  fta1glem2  23907  fta1blem  23909  ig1peu  23912  ig1pdvds  23917  dgrmulc  24008  dgrcolem1  24010  plydivlem4  24032  plydiveu  24034  fta1lem  24043  vieta1lem1  24046  vieta1lem2  24047  plyexmo  24049  taylfvallem1  24092  taylfval  24094  tayl0  24097  taylplem1  24098  taylply2  24103  taylply  24104  dvtaylp  24105  dvntaylp  24106  dvntaylp0  24107  taylthlem1  24108  taylthlem2  24109  ulmcaulem  24129  ulmcau  24130  ulmcn  24134  ulmdvlem1  24135  radcnvlem1  24148  radcnvle  24155  psercn  24161  pserdvlem2  24163  pserdv  24164  abelth  24176  cosordlem  24258  tanregt0  24266  dvlog2lem  24379  efopn  24385  logtayllem  24386  logccv  24390  cxplt3  24427  cxpmul2zd  24443  cxpltd  24446  cxpled  24447  cxplt3d  24459  cxple3d  24460  dvsqrt  24464  cxpcn3  24470  cxpaddle  24474  cxpeq  24479  angcan  24513  angvald  24515  ang180lem2  24521  ang180  24525  isosctrlem3  24531  dquartlem1  24559  atantayl2  24646  leibpilem1  24648  leibpi  24650  log2tlbnd  24653  birthdaylem3  24661  xrlimcnp  24676  efrlim  24677  o1cxp  24682  jensenlem2  24695  jensen  24696  fsumharmonic  24719  lgamucov  24745  lgamcvg2  24762  wilthlem1  24775  basellem3  24790  basellem6  24793  basellem8  24795  ppisval  24811  chtwordi  24863  ppiwordi  24869  mumullem2  24887  dvdsmulf1o  24901  fsumvma  24919  fsumvma2  24920  chpchtsum  24925  chpub  24926  logfacubnd  24927  dchrmulcl  24955  dchrinv  24967  dchrptlem1  24970  dchrptlem2  24971  sumdchr2  24976  dchr2sum  24979  bposlem7  24996  lgslem1  25003  lgslem3  25005  lgsdirprm  25037  lgsqrlem2  25053  lgseisenlem1  25081  lgseisenlem2  25082  lgseisenlem4  25084  lgseisen  25085  lgsquadlem1  25086  lgsquad2lem1  25090  lgsquad3  25093  m1lgs  25094  2sqlem7  25130  chebbnd1lem2  25140  chebbnd1lem3  25141  rplogsumlem1  25154  rpvmasumlem  25157  dchrvmasumlem1  25165  dchrvmasum2lem  25166  dchrvmasumlema  25170  dchrisum0flblem2  25179  dchrisum0fno1  25181  dchrisum0re  25183  logdivsum  25203  pntrsumbnd2  25237  pntpbnd1a  25255  pntpbnd1  25256  pntibndlem2  25261  pntlemr  25272  pntlemj  25273  pntlemf  25275  pnt2  25283  padicabv  25300  ostth2lem2  25304  f1otrg  25732  brbtwn2  25766  colinearalglem2  25768  axcgrtr  25776  axcgrid  25777  axsegconlem7  25784  axsegcon  25788  ax5seglem3  25792  ax5seglem6  25795  ax5seg  25799  axpaschlem  25801  axlowdimlem17  25819  axcontlem2  25826  axcontlem4  25828  axcontlem7  25831  axcontlem8  25832  ecgrtg  25844  usgredg2v  26100  vtxdgoddnumeven  26430  2trlond  26816  eupthp1  27056  numclwwlkovf2ex  27191  nmobndi  27600  ubthlem2  27697  ubthlem3  27698  minvecolem2  27701  shuni  28129  pjhthlem1  28220  chscllem2  28467  pjcompi  28501  mayete3i  28557  unoplin  28749  hmoplin  28771  nmophmi  28860  mdslmd4i  29162  isoun  29453  xrge0addcld  29501  xrofsup  29507  eliccelico  29513  elicoelioo  29514  difioo  29518  rexdiv  29608  2sqmod  29622  xrge0addgt0  29665  omndadd2d  29682  omndadd2rd  29683  omndmul2  29686  ofldchr  29788  mdetpmtr2  29864  mdetpmtr12  29865  madjusmdetlem1  29867  madjusmdetlem4  29870  unitdivcld  29921  xrge0mulc1cn  29961  qqhnm  30008  esumcst  30099  esumfsup  30106  esumpmono  30115  esumcvg  30122  difelsiga  30170  sigapisys  30192  sigapildsys  30199  ldgenpisyslem1  30200  1stmbfm  30296  2ndmbfm  30297  dya2icoseg  30313  sibfinima  30375  probmeasb  30466  orvcgteel  30503  orvclteel  30508  ballotlemsima  30551  ballotlemfrceq  30564  sgnmul  30578  ccatmulgnn0dir  30593  fct2relem  30649  ftc2re  30650  chtvalz  30681  subfacp1lem2a  31136  subfaclim  31144  erdsze2lem2  31160  cvmliftlem2  31242  cvmliftlem10  31250  cvmliftlem13  31252  cvmliftiota  31257  cvmlift2lem9  31267  cvmlift2lem11  31269  cvmlift2lem12  31270  cvmliftphtlem  31273  cvmlift3lem6  31280  cvmlift3lem7  31281  cvmlift3lem9  31283  snmlff  31285  mrsubfval  31379  trpredelss  31706  trpredpo  31709  wzel  31745  wzelOLD  31746  wsuclem  31747  wsuclemOLD  31748  sltrec  31898  brsegle  32190  opnregcld  32300  addgtge0d  32471  fin2so  33367  poimirlem17  33397  poimirlem23  33403  opnmbllem0  33416  mblfinlem3  33419  mblfinlem4  33420  itg2addnclem  33432  itg2addnc  33435  itg2gt0cn  33436  ftc1cnnclem  33454  ftc1cnnc  33455  areacirclem5  33475  indexdom  33500  sstotbnd2  33544  isbnd3  33554  isbnd3b  33555  cntotbnd  33566  ismtyima  33573  heibor1lem  33579  heiborlem8  33588  rrncmslem  33602  reheibor  33609  lkrlsp  34208  lshpkrlem5  34220  ldualssvscl  34264  ldualssvsubcl  34265  llnmlplnN  34644  llncvrlpln  34663  pmapjat1  34958  pclfinN  35005  lautlt  35196  lauteq  35200  lautco  35202  ltrn11  35231  ltrnle  35234  ltrneq2  35253  cdlemednuN  35406  cdleme20k  35426  cdleme20l2  35428  cdleme20l  35429  cdleme20m  35430  cdleme21c  35434  cdleme22e  35451  cdleme22eALTN  35452  cdlemefrs32fva  35507  cdlemg4g  35723  cdlemg18b  35786  cdlemg18c  35787  cdlemj3  35930  dia2dimlem5  36176  dvhopN  36224  cdlemm10N  36226  dihjatcclem4  36529  dochexmidlem2  36569  lclkrlem2o  36629  lcfrlem5  36654  lcfrlem6  36655  lcdlssvscl  36714  mapdpglem6  36786  mapdpglem9  36788  mapdpglem12  36791  mapdpglem14  36793  mapdindp0  36827  hdmaprnlem7N  36966  hdmaprnlem8N  36967  hdmaprnlem3eN  36969  hgmapvvlem3  37036  mzpsubst  37130  eldioph2lem1  37142  eldioph2lem2  37143  eldioph2b  37145  diophin  37155  irrapxlem2  37206  irrapxlem4  37208  irrapxlem5  37209  pellexlem1  37212  pellexlem2  37213  pellexlem6  37217  elpell1qr2  37255  pell1qrgaplem  37256  pell1qrgap  37257  pellqrex  37262  pellfundex  37269  pellfund14  37281  rmspecsqrtnq  37289  rmspecsqrtnqOLD  37290  rmxyadd  37305  expmordi  37331  rmxypos  37333  jm2.24  37349  congsub  37356  mzpcong  37358  congrep  37359  acongtr  37364  acongrep  37366  jm2.19lem1  37375  jm2.22  37381  jm2.23  37382  jm2.26lem3  37387  jm2.26  37388  jm2.27a  37391  fnwe2lem2  37440  aomclem6  37448  hbtlem2  37513  hbtlem4  37515  hbtlem5  37517  dgraa0p  37538  rngunsnply  37562  acsfn1p  37588  proot1hash  37597  itgpowd  37619  expgrowth  38354  abslt2sqd  39389  ioondisj2  39517  ioondisj1  39518  eliocre  39537  ioossioobi  39546  iooiinicc  39572  iooiinioc  39586  icossico2  39594  lptioo2  39663  limcresiooub  39674  limsupequzlem  39754  cncfuni  39862  cncfiooicclem1  39869  cxpcncf2  39876  dvcnre  39893  dvresntr  39895  dvmptresicc  39897  dvresioo  39899  dvbdfbdioolem1  39906  dvnmptdivc  39916  dvnxpaek  39920  itgsinexplem1  39932  itgcoscmulx  39948  itgiccshift  39959  itgperiod  39960  ovolsplit  39968  stoweidlem11  39991  stoweidlem26  40006  stoweidlem34  40014  stoweidlem36  40016  stoweidlem38  40018  stirlinglem5  40058  dirkercncflem2  40084  dirkercncflem4  40086  fourierdlem20  40107  fourierdlem58  40144  fourierdlem72  40158  fourierdlem73  40159  fourierdlem74  40160  fourierdlem75  40161  fourierdlem76  40162  fourierdlem79  40165  fourierdlem80  40166  fourierdlem87  40173  fourierdlem94  40180  fourierdlem103  40189  fourierdlem104  40190  fourierdlem107  40193  fourierdlem113  40199  sqwvfoura  40208  sqwvfourb  40209  fourierswlem  40210  fouriersw  40211  etransclem46  40260  etransclem47  40261  rrndistlt  40273  rrnprjdstle  40284  ioorrnopnxrlem  40289  sge0ssre  40377  sge0seq  40426  hsphoidmvle2  40562  hsphoidmvle  40563  hoidmv1lelem1  40568  hoidmv1lelem2  40569  hoidmv1lelem3  40570  hoidmvlelem1  40572  hoidifhspdmvle  40597  hoiqssbllem2  40600  ovolval5lem2  40630  iinhoiicc  40651  iunhoiioo  40653  vonioolem2  40658  vonicclem2  40661  issmflem  40699  iccpartdisj  41137  m1expevenALTV  41325  oexpnegALTV  41353  tgoldbach  41470  tgoldbachOLD  41477  nn0eo  42087  fdivpm  42102  refdivpm  42103  elbigolo1  42116  logbpw2m1  42126  fllog2  42127  dignn0flhalflem1  42174  dignn0flhalflem2  42175
  Copyright terms: Public domain W3C validator