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

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

Proof of Theorem syl21anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 3jca31 556 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anc.4 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
64, 5syl 17 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  wereu2  5140  funprgOLD  5979  funtpg  5980  funtpgOLD  5981  funcnvtp  5989  funcnvqp  5990  funcnvqpOLD  5991  fnunsn  6036  fun2d  6106  fresaun  6113  fvun1  6308  iinpreima  6385  ftpg  6463  fsnunf  6492  f1prex  6579  soisores  6617  isotr  6626  off  6954  caofrss  6972  caonncan  6977  fvmpt2curryd  7442  oaf1o  7688  omeulem1  7707  oeordi  7712  oelimcl  7725  oeeulem  7726  oeeui  7727  oaabs2  7770  omabs  7772  pmresg  7927  ralxpmap  7949  domunsncan  8101  mapunen  8170  sucdom2  8197  unxpdom2  8209  sucxpdom  8210  ac6sfi  8245  unblem4  8256  fodomfi  8280  hartogslem1  8488  brwdom2  8519  cantnflt  8607  cantnflem3  8626  cantnflem4  8627  cnfcomlem  8634  cnfcom  8635  infxpenlem  8874  infxpenc  8879  fseqenlem1  8885  pwsdompw  9064  cfeq0  9116  cofsmo  9129  cfsmolem  9130  ssfin4  9170  hsmexlem4  9289  hsmexlem5  9290  axdc3lem2  9311  axdc3lem4  9313  fpwwe2  9503  wunpr  9569  mulclpi  9753  mulcanenq  9820  distrlem4pr  9886  prlem934  9893  prlem936  9907  divge0d  11950  fseq1p1m1  12452  elfznelfzob  12614  seqcaopr2  12877  facavg  13128  cats1un  13521  f1oun2prg  13708  sqrtdiv  14050  sqrtdivd  14206  mulcn2  14370  o1of2  14387  fsumsplit  14515  sumsplit  14543  isumless  14621  demoivreALT  14975  rpnnen2lem11  14997  gcdnncl  15276  qredeu  15419  rpdvds  15421  isprm5  15466  rpexp  15479  divnumden  15503  divdenle  15504  phimullem  15531  phisum  15542  pythagtriplem4  15571  pythagtriplem8  15575  pythagtriplem9  15576  pcgcd1  15628  sumhash  15647  fldivp1  15648  pockthlem  15656  setsfun  15940  setsfun0  15941  ssc2  16529  estrreslem1  16824  mndpropd  17363  grpidssd  17538  grpinvssd  17539  issubg2  17656  isnsg3  17675  eqgid  17693  gass  17780  symgextres  17891  gsmsymgreqlem2  17897  sylow1lem5  18063  sylow2alem2  18079  sylow3lem3  18090  efgredlemd  18203  efgredlem  18206  frgpnabllem1  18322  frgpnabllem2  18323  subgdmdprd  18479  ablfacrplem  18510  kerf1hrm  18791  issrngd  18909  lmodprop2d  18973  lsspropd  19065  pwssplit1  19107  lspvadd  19144  mplsubglem  19482  mplind  19550  znidomb  19958  znrrg  19962  lindfind  20203  lindsind  20204  mat1ghm  20337  mdetunilem1  20466  mdetunilem3  20468  mdetunilem4  20469  mdetunilem9  20474  cramerimplem2  20538  mat2pmatlin  20588  monmatcollpw  20632  cpmadugsumlemF  20729  mretopd  20944  neiptopnei  20984  neitr  21032  ufilen  21781  flimrest  21834  flimclslem  21835  fclsrest  21875  cnextcn  21918  haustsms2  21987  tsmsxplem2  22004  trust  22080  utoptop  22085  restutop  22088  ustuqtop4  22095  utopsnneiplem  22098  utop2nei  22101  utop3cls  22102  isucn2  22130  ucnima  22132  ucncn  22136  fmucnd  22143  trcfilu  22145  comet  22365  metustexhalf  22408  metustbl  22418  psmetutop  22419  nrmmetd  22426  reconnlem1  22676  reconnlem2  22677  fsumcn  22720  cmetcaulem  23132  iscmet3lem1  23135  iscmet3lem2  23136  bcthlem5  23171  rrxdstprj1  23238  minveclem4  23249  ovolfiniun  23315  itg1addlem4  23511  itg1addlem5  23512  itgsplitioo  23649  c1liplem1  23804  dvfsumlem1  23834  plyeq0lem  24011  quotcan  24109  psercnlem1  24224  cxplea  24487  birthdaylem3  24725  musumsum  24963  dvdsmulf1o  24965  dchrelbas4  25013  dchrhash  25041  gausslemma2dlem0d  25129  gausslemma2dlem1a  25135  2lgslem1a1  25159  2sqlem8a  25195  2sqlem8  25196  chto1ub  25210  vmadivsum  25216  dchrisumlem1  25223  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  rpvmasum2  25246  mulog2sumlem2  25269  selberg2lem  25284  pntrmax  25298  pntpbnd1  25320  pntlemb  25331  pntlemj  25337  ercgrg  25457  tgcgr4  25471  motcgr  25476  tglineeltr  25571  colline  25589  miriso  25610  midexlem  25632  perpneq  25654  foot  25659  f1otrg  25796  f1otrge  25797  axcontlem9  25897  uspgr1ewop  26185  nbupgrres  26310  structtocusgr  26398  wlkp1  26634  clwlkl1loop  26734  uspgrn2crct  26756  crctcshwlkn0lem5  26762  3trlond  27151  3pthond  27153  3spthond  27155  frgr3v  27255  vdgn1frgrv2  27276  numclwwlk3  27372  nmblolbii  27782  minvecolem3  27860  minvecolem4  27864  htthlem  27902  bcs2  28167  nmopub2tALT  28896  nmfnleub2  28913  eighmorth  28951  nmophmi  29018  nmopcoadji  29088  hstle  29217  atcvat3i  29383  disjxpin  29527  fmptco1f1o  29562  off2  29571  xppreima2  29578  fgreu  29599  1stpreimas  29611  padct  29625  resf1o  29633  fpwrelmap  29636  xrofsup  29661  eliccelico  29667  elicoelioo  29668  iocinif  29671  difioo  29672  2sqcoprm  29775  2sqmod  29776  ressprs  29783  tleile  29789  xrge0addgt0  29819  xrge0adddir  29820  omndmul3  29841  archirng  29870  archirngz  29871  gsumle  29907  orngmul  29931  1smat1  29998  madjusmdetlem2  30022  qtophaus  30031  locfinref  30036  metideq  30064  sqsscirc2  30083  tpr2rico  30086  fmcncfil  30105  lmxrge0  30126  lmdvg  30127  qqhval2lem  30153  qqhf  30158  qqhnm  30162  esumle  30248  gsumesum  30249  esumlef  30252  esumrnmpt2  30258  esumpcvgval  30268  esum2d  30283  ofcf  30293  ldsysgenld  30351  ldgenpisyslem1  30354  unelros  30362  difelros  30363  inelsros  30369  diffiunisros  30370  imambfm  30452  omssubadd  30490  inelcarsg  30501  carsgsigalem  30505  carsggect  30508  carsgclctunlem2  30509  oddpwdc  30544  eulerpartlems  30550  eulerpartlemb  30558  eulerpartlemt  30561  iwrdsplit  30577  sseqfn  30580  sseqf  30582  sseqfres  30583  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemfrcn0  30719  sgnsub  30734  plymulx0  30752  signsplypnf  30755  signsvtn0  30775  signstfvneq0  30777  signsvtp  30788  signsvtn  30789  fsum2dsub  30813  reprlt  30825  hashreprin  30826  reprgt  30827  reprpmtf1o  30832  chtvalz  30835  breprexplema  30836  breprexplemc  30838  breprexp  30839  circlemeth  30846  logdivsqrle  30856  hgt750lemb  30862  bnj927  30965  bnj1536  31050  bnj1001  31154  bnj1280  31214  cvxsconn  31351  elmrsubrn  31543  frpomin  31863  noextend  31944  neibastop3  32482  finxpsuclem  33364  poimirlem16  33555  poimirlem19  33558  poimirlem20  33559  poimirlem29  33568  mblfinlem3  33578  itg2addnclem3  33593  ftc1cnnclem  33613  lautlt  35695  lautcvr  35696  lauteq  35699  lautco  35701  ltrncl  35729  ltrncnvleN  35734  trljat2  35772  cdlemc6  35801  cdleme20c  35916  cdleme20j  35923  cdleme22e  35949  cdleme22eALTN  35950  cdlemg7aN  36230  cdlemg12e  36252  cdlemg17dALTN  36269  cdlemh  36422  cdlemkfid1N  36526  dibglbN  36772  diblss  36776  diclspsn  36800  dih1  36892  dihglbcpreN  36906  dihmeetlem4preN  36912  lcfrlem19  37167  mapfzcons  37596  mzpcl34  37611  mzpindd  37626  mzpsubst  37628  diophrw  37639  diophren  37694  irrapxlem1  37703  pellexlem5  37714  acongrep  37864  pwssplit4  37976  brtrclfv2  38336  rfovcnvf1od  38615  ntrk0kbimka  38654  isotone1  38663  isotone2  38664  4an4132  39022  mulltgt0  39495  fnchoice  39502  3adantlr3  39514  3adantll2  39516  3adantll3  39517  uzwo4  39535  disjf1o  39692  supxrgelem  39866  infleinflem2  39900  xrralrecnnle  39915  supxrunb3  39936  unb2ltle  39955  infrpgernmpt  40008  iooiinicc  40087  iooiinioc  40101  fmuldfeq  40133  mccl  40148  limccog  40170  limcrecl  40179  lptioo1  40182  islpcn  40189  limsupre  40191  neglimc  40197  0ellimcdiv  40199  limclner  40201  climleltrp  40226  climinf3  40266  liminflimsupclim  40357  icccncfext  40418  fprodcncf  40432  dvnmptdivc  40471  dvnmul  40476  dvmptfprod  40478  dvnprodlem3  40481  stoweidlem25  40560  stoweidlem34  40569  stoweidlem38  40573  stoweidlem44  40579  stoweidlem48  40583  stoweidlem49  40584  stoweidlem59  40594  stoweidlem60  40595  wallispilem4  40603  stirlinglem5  40613  dirkercncflem2  40639  fourierdlem39  40681  fourierdlem42  40684  fourierdlem46  40687  fourierdlem47  40688  fourierdlem48  40689  fourierdlem50  40691  fourierdlem51  40692  fourierdlem64  40705  fourierdlem73  40714  fourierdlem74  40715  fourierdlem77  40718  fourierdlem80  40721  fourierdlem87  40728  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  etransclem32  40801  rrxsnicc  40838  sge0cl  40916  sge0f1o  40917  nnfoctbdjlem  40990  ismeannd  41002  omeiunltfirp  41054  hoicvr  41083  ovncvrrp  41099  hoidmvlelem2  41131  hoidmvlelem5  41134  hspdifhsp  41151  hoiqssbllem2  41158  hspmbllem2  41162  vonicclem2  41219  smflimsuplem7  41353  sqrtpwpw2p  41775  lincresunit2  42592  nnpw2pmod  42702  dignn0flhalflem1  42734  dignn0flhalf  42737
  Copyright terms: Public domain W3C validator