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

Theorem syl122anc 1491
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl122anc.6 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
Assertion
Ref Expression
syl122anc (𝜑𝜁)

Proof of Theorem syl122anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 503 . 2 (𝜑 → (𝜏𝜂))
7 syl122anc.6 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl121anc 1487 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  divdiv32d  11114  divcan5d  11115  divcan7d  11117  divdiv1d  11120  divdiv2d  11121  seqcoll  13468  cau3lem  14320  eqsqrtd  14333  isercolllem2  14622  isercoll  14624  summolem2a  14672  divrcnv  14809  prodmolem2a  14888  prmind2  15619  divnumden  15676  pceulem  15770  pcqmul  15778  pcqdiv  15782  pcexp  15784  pcaddlem  15812  pcbc  15824  prmodvdslcmf  15971  latledi  17297  latjjdi  17311  latjjdir  17312  sylow1lem1  18217  sylow1lem5  18221  efgred2  18370  abladdsub4  18423  ablpnpcan  18429  ghmplusg  18453  frgpnabllem2  18481  isabvd  19027  lmodvs1  19098  lspsolvlem  19353  evlslem1  19726  frgpcyg  20132  ip2di  20199  mdetuni0  20642  cpmadugsumlemB  20896  elptr2  21595  blss2ps  22425  blss2  22426  blssps  22446  blss  22447  xmeter  22455  metdcnlem  22856  lebnumii  22982  minveclem2  23415  pjthlem1  23426  volfiniun  23534  dvfsumrlimge0  24013  lgsdi  25279  ax5seglem3  26031  ax5seglem6  26034  axcontlem8  26071  eengtrkg  26085  vacn  27883  minvecolem2  28065  minvecolem4  28070  disjabrex  29726  disjabrexf  29727  slmdvs1  30104  slmd0vs  30108  orngsqr  30135  ornglmulle  30136  orngrmulle  30137  orngmullt  30140  suborng  30146  madjusmdetlem1  30224  cgrcomand  32424  cgrcomr  32430  cgrcomland  32432  cgrcomrand  32433  cgrtriv  32435  cgrid2  32436  ofscom  32440  cgrextend  32441  segconeq  32443  btwntriv2  32445  btwnexch3and  32454  btwnouttr2  32455  btwnouttr  32457  btwnexch  32458  btwnexchand  32459  btwndiff  32460  ifscgr  32477  cgrsub  32478  cgrxfr  32488  lineext  32509  endofsegid  32518  btwnconn1lem2  32521  btwnconn1lem3  32522  btwnconn1lem4  32523  btwnconn1lem5  32524  btwnconn1lem7  32526  btwnconn1lem8  32527  btwnconn1lem10  32529  btwnconn1lem11  32530  btwnconn1lem13  32532  btwnconn1lem14  32533  btwnconn3  32536  midofsegid  32537  segcon2  32538  brsegle2  32542  seglecgr12im  32543  seglecgr12  32544  seglerflx  32545  seglemin  32546  segletr  32547  btwnsegle  32550  colinbtwnle  32551  btwnoutside  32558  broutsideof3  32559  outsideoftr  32562  outsideofeq  32563  outsidele  32565  lineunray  32580  lineelsb2  32581  lfladdcl  34853  lshpkrlem4  34895  latmmdiN  35016  latmmdir  35017  hlatj4  35156  4atlem4b  35382  4atlem11  35391  4atlem12  35394  dalem2  35443  dalem-cly  35453  dalem10  35455  dalem23  35478  dalem38  35492  dalem44  35498  dalem55  35509  cdlema1N  35573  paddclN  35624  pmapjoin  35634  dalawlem3  35655  dalawlem5  35657  dalawlem7  35659  dalawlem8  35660  dalawlem11  35663  dalawlem12  35664  lhpexle3lem  35793  4atexlemc  35851  trlnidat  35955  arglem1N  35972  cdlemd9  35988  cdleme0moN  36007  cdleme11c  36043  cdleme11h  36048  cdleme11  36052  cdleme16c  36062  cdleme16f  36065  cdlemeda  36080  cdleme20l2  36103  cdlemefs32sn1aw  36196  cdleme43fsv1snlem  36202  cdleme41sn3a  36215  cdleme32fva  36219  cdleme32b  36224  cdleme32c  36225  cdleme32e  36227  cdleme40m  36249  cdleme40n  36250  cdleme42e  36261  cdleme48d  36317  cdlemf2  36344  cdlemf  36345  cdlemg2fv2  36382  cdlemg7fvbwN  36389  cdlemg7fvN  36406  cdlemg9a  36414  cdlemg9b  36415  cdlemg10a  36422  cdlemg12b  36426  cdlemg17b  36444  cdlemg31d  36482  cdlemg33b0  36483  cdlemg33a  36488  ltrnco  36501  ltrncom  36520  cdlemh  36599  cdlemk3  36615  cdlemk12  36632  cdlemk12u  36654  cdlemkfid1N  36703  cdlemk51  36735  cdlemk54  36740  cdlemk43N  36745  cdlemk35u  36746  cdlemk55u1  36747  cdlemk39u1  36749  cdlemk19u1  36751  dia2dimlem10  36855  dvhgrp  36889  dvh0g  36893  cdlemm10N  36900  diblsmopel  36953  cdlemn4  36980  cdlemn6  36984  cdlemn7  36985  dihordlem7  36996  dihord1  37000  dihord2pre  37007  dihvalcqat  37021  dihopelvalcpre  37030  dihord5apre  37044  dihord  37046  dih1  37068  dihglbcpreN  37082  dihjatc1  37093  dihmeetlem13N  37101  dihmeetALTN  37109  dihjatcclem1  37200  baerlem3lem1  37489  pellfundex  37953  rmxypairf1o  37978  rmxycomplete  37984  rmxyneg  37987  rmxyadd  37988  rmxy1  37989  rmxy0  37990  jm2.22  38064  proot1mul  38279  deg1mhm  38287  stoweidlem7  40704  stoweidlem36  40733
  Copyright terms: Public domain W3C validator