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

Theorem syl21anc 1316
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 554 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anc.4 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
64, 5syl 17 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  wereu2  5025  funprgOLD  5841  funtpg  5842  funtpgOLD  5843  funcnvtp  5851  funcnvqp  5852  funcnvqpOLD  5853  fnunsn  5898  fresaun  5973  fvun1  6164  iinpreima  6238  ftpg  6306  fsnunf  6334  f1prex  6417  soisores  6455  isotr  6464  off  6788  caofrss  6806  caonncan  6811  fvmpt2curryd  7262  oaf1o  7508  omeulem1  7527  oeordi  7532  oelimcl  7545  oeeulem  7546  oeeui  7547  oaabs2  7590  omabs  7592  pmresg  7749  ralxpmap  7771  domunsncan  7923  mapunen  7992  sucdom2  8019  unxpdom2  8031  sucxpdom  8032  ac6sfi  8067  unblem4  8078  fodomfi  8102  hartogslem1  8308  brwdom2  8339  cantnflt  8430  cantnflem3  8449  cantnflem4  8450  cnfcomlem  8457  cnfcom  8458  infxpenlem  8697  infxpenc  8702  fseqenlem1  8708  pwsdompw  8887  cfeq0  8939  cofsmo  8952  cfsmolem  8953  ssfin4  8993  hsmexlem4  9112  hsmexlem5  9113  axdc3lem2  9134  axdc3lem4  9136  fpwwe2  9322  wunpr  9388  mulclpi  9572  mulcanenq  9639  distrlem4pr  9705  prlem934  9712  prlem936  9726  divge0d  11747  fseq1p1m1  12241  elfznelfzob  12398  seqcaopr2  12657  facavg  12908  cats1un  13276  f1oun2prg  13461  sqrtdiv  13803  sqrtdivd  13959  mulcn2  14123  o1of2  14140  fsumsplit  14267  sumsplit  14290  isumless  14365  demoivreALT  14719  rpnnen2lem11  14741  gcdnncl  15016  qredeu  15159  rpdvds  15161  isprm5  15206  rpexp  15219  divnumden  15243  divdenle  15244  phimullem  15271  phisum  15282  pythagtriplem4  15311  pythagtriplem8  15315  pythagtriplem9  15316  pcgcd1  15368  sumhash  15387  fldivp1  15388  pockthlem  15396  setsfun  15674  setsfun0  15675  ssc2  16254  estrreslem1  16549  mndpropd  17088  grpidssd  17263  grpinvssd  17264  issubg2  17381  isnsg3  17400  eqgid  17418  gass  17506  symgextres  17617  gsmsymgreqlem2  17623  sylow1lem5  17789  sylow2alem2  17805  sylow3lem3  17816  efgredlemd  17929  efgredlem  17932  frgpnabllem1  18048  frgpnabllem2  18049  subgdmdprd  18205  ablfacrplem  18236  kerf1hrm  18515  issrngd  18633  lmodprop2d  18697  lsspropd  18787  pwssplit1  18829  lspvadd  18866  mplsubglem  19204  mplind  19272  znidomb  19677  znrrg  19681  lindfind  19922  lindsind  19923  mat1ghm  20056  mdetunilem1  20185  mdetunilem3  20187  mdetunilem4  20188  mdetunilem9  20193  cramerimplem2  20257  mat2pmatlin  20307  monmatcollpw  20351  cpmadugsumlemF  20448  mretopd  20654  neiptopnei  20694  neitr  20742  ufilen  21492  flimrest  21545  flimclslem  21546  fclsrest  21586  cnextcn  21629  haustsms2  21698  tsmsxplem2  21715  trust  21791  utoptop  21796  restutop  21799  ustuqtop4  21806  utopsnneiplem  21809  utop2nei  21812  utop3cls  21813  isucn2  21841  ucnima  21843  ucncn  21847  fmucnd  21854  trcfilu  21856  comet  22076  metustexhalf  22119  metustbl  22129  psmetutop  22130  nrmmetd  22137  reconnlem1  22385  reconnlem2  22386  fsumcn  22429  cmetcaulem  22839  iscmet3lem1  22842  iscmet3lem2  22843  bcthlem5  22878  rrxdstprj1  22945  minveclem4  22956  ovolfiniun  23021  itg1addlem4  23217  itg1addlem5  23218  itgsplitioo  23355  c1liplem1  23508  dvfsumlem1  23538  plyeq0lem  23715  quotcan  23813  psercnlem1  23928  cxplea  24187  birthdaylem3  24425  musumsum  24663  dvdsmulf1o  24665  dchrelbas4  24713  dchrhash  24741  gausslemma2dlem0d  24829  gausslemma2dlem1a  24835  2lgslem1a1  24859  2sqlem8a  24895  2sqlem8  24896  chto1ub  24910  vmadivsum  24916  dchrisumlem1  24923  dchrvmasumlem2  24932  dchrvmasumiflem1  24935  rpvmasum2  24946  mulog2sumlem2  24969  selberg2lem  24984  pntrmax  24998  pntpbnd1  25020  pntlemb  25031  pntlemj  25037  ercgrg  25158  tgcgr4  25172  motcgr  25177  tglineeltr  25272  colline  25290  miriso  25311  midexlem  25333  perpneq  25355  foot  25360  f1otrg  25497  f1otrge  25498  axcontlem9  25598  uhgraun  25634  umgraun  25651  2wlklemA  25878  2wlklemB  25879  2wlklemC  25880  constr3trllem3  25974  vdgrun  26222  vdgrfiun  26223  eupap1  26297  nmblolbii  26872  minvecolem3  26950  minvecolem4  26954  htthlem  26992  bcs2  27257  nmopub2tALT  27986  nmfnleub2  28003  eighmorth  28041  nmophmi  28108  nmopcoadji  28178  hstle  28307  atcvat3i  28473  disjxpin  28617  off2  28657  xppreima2  28664  fgreu  28688  1stpreimas  28700  padct  28719  resf1o  28727  fpwrelmap  28730  xrofsup  28757  eliccelico  28763  elicoelioo  28764  iocinif  28767  difioo  28768  2sqcoprm  28812  2sqmod  28813  ressprs  28820  tleile  28826  xrge0addgt0  28856  xrge0adddir  28857  omndmul3  28878  archirng  28907  archirngz  28908  gsumle  28944  orngmul  28968  1smat1  29032  madjusmdetlem2  29056  qtophaus  29065  locfinref  29070  metideq  29098  sqsscirc2  29117  tpr2rico  29120  fmcncfil  29139  lmxrge0  29160  lmdvg  29161  qqhval2lem  29187  qqhf  29192  qqhnm  29196  esumle  29281  gsumesum  29282  esumlef  29285  esumrnmpt2  29291  esumpcvgval  29301  esum2d  29316  ofcf  29326  ldsysgenld  29384  ldgenpisyslem1  29387  unelros  29395  difelros  29396  inelsros  29402  diffiunisros  29403  imambfm  29485  omssubadd  29523  inelcarsg  29534  carsgsigalem  29538  carsggect  29541  carsgclctunlem2  29542  oddpwdc  29577  eulerpartlems  29583  eulerpartlemb  29591  eulerpartlemt  29594  iwrdsplit  29610  sseqfn  29613  sseqf  29615  sseqfres  29616  ballotlemfc0  29715  ballotlemfcc  29716  ballotlemfrcn0  29752  sgnsub  29767  plymulx0  29784  signsplypnf  29787  signsvtn0  29807  signstfvneq0  29809  signsvtp  29820  signsvtn  29821  bnj927  29927  bnj1536  30012  bnj1001  30116  bnj1280  30176  cvxscon  30313  elmrsubrn  30505  nobndup  30933  nobnddown  30934  neibastop3  31361  finxpsuclem  32234  poimirlem16  32419  poimirlem19  32422  poimirlem20  32423  poimirlem29  32432  mblfinlem3  32442  itg2addnclem3  32457  ftc1cnnclem  32477  lautlt  34219  lautcvr  34220  lauteq  34223  lautco  34225  ltrncl  34253  ltrncnvleN  34258  trljat2  34296  cdlemc6  34325  cdleme20c  34441  cdleme20j  34448  cdleme22e  34474  cdleme22eALTN  34475  cdlemg7aN  34755  cdlemg12e  34777  cdlemg17dALTN  34794  cdlemh  34947  cdlemkfid1N  35051  dibglbN  35297  diblss  35301  diclspsn  35325  dih1  35417  dihglbcpreN  35431  dihmeetlem4preN  35437  lcfrlem19  35692  mapfzcons  36121  mzpcl34  36136  mzpindd  36151  mzpsubst  36153  diophrw  36164  diophren  36219  irrapxlem1  36228  pellexlem5  36239  acongrep  36389  pwssplit4  36501  brtrclfv2  36862  rfovcnvf1od  37142  ntrk0kbimka  37181  isotone1  37190  isotone2  37191  4an4132  37550  mulltgt0  38028  fnchoice  38035  3adantlr3  38047  3adantll2  38049  3adantll3  38050  uzwo4  38070  disjf1o  38197  supxrgelem  38318  infleinflem2  38352  xrralrecnnle  38367  iooiinicc  38440  iooiinioc  38454  fmuldfeq  38474  mccl  38489  limccog  38511  limcrecl  38520  lptioo1  38523  islpcn  38530  limsupre  38532  neglimc  38538  0ellimcdiv  38540  limclner  38542  climleltrp  38567  icccncfext  38597  fprodcncf  38611  dvnmptdivc  38652  dvnmul  38657  dvmptfprod  38659  dvnprodlem3  38662  stoweidlem25  38742  stoweidlem34  38751  stoweidlem38  38755  stoweidlem44  38761  stoweidlem48  38765  stoweidlem49  38766  stoweidlem59  38776  stoweidlem60  38777  wallispilem4  38785  stirlinglem5  38795  dirkercncflem2  38821  fourierdlem39  38863  fourierdlem42  38866  fourierdlem46  38869  fourierdlem47  38870  fourierdlem48  38871  fourierdlem50  38873  fourierdlem51  38874  fourierdlem64  38887  fourierdlem73  38896  fourierdlem74  38897  fourierdlem77  38900  fourierdlem80  38903  fourierdlem87  38910  fourierdlem94  38917  fourierdlem103  38926  fourierdlem104  38927  etransclem32  38983  rrxsnicc  39020  sge0cl  39098  sge0f1o  39099  nnfoctbdjlem  39172  ismeannd  39184  omeiunltfirp  39233  hoicvr  39262  ovncvrrp  39278  hoidmvlelem2  39310  hoidmvlelem5  39313  hspdifhsp  39330  hoiqssbllem2  39337  hspmbllem2  39341  vonicclem2  39399  fdisjdmun  39682  sqrtpwpw2p  39813  uspgr1ewop  40496  nbupgrres  40614  1wlkp1  40912  clwlkl1loop  41011  uspgrn2crct  41033  crctcsh1wlkn0lem5  41039  3trlond  41362  3pthond  41364  3spthond  41366  frgr3v  41467  vdgn1frgrv2  41488  av-numclwwlk3  41561  lincresunit2  42083  nnpw2pmod  42197  dignn0flhalflem1  42229  dignn0flhalf  42232
  Copyright terms: Public domain W3C validator