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

Theorem syl122anc 1380
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 513 . 2 (𝜑 → (𝜏𝜂))
7 syl122anc.6 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl121anc 1376 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  divdiv32d  11964  divcan5d  11965  divcan7d  11967  divdiv1d  11970  divdiv2d  11971  seqcoll  14372  cau3lem  15248  eqsqrtd  15261  isercolllem2  15559  isercoll  15561  summolem2a  15608  divrcnv  15745  prodmolem2a  15825  prmind2  16569  divnumden  16631  pceulem  16725  pcqmul  16733  pcqdiv  16737  pcexp  16739  pcaddlem  16768  pcbc  16780  prmodvdslcmf  16927  latledi  18374  latjjdi  18388  latjjdir  18389  sylow1lem1  19388  sylow1lem5  19392  efgred2  19543  abladdsub4  19600  ablpnpcan  19606  ghmplusg  19632  frgpnabllem2  19660  isabvd  20322  lmodvs1  20394  lspsolvlem  20648  frgpcyg  21003  ip2di  21068  evlslem1  21515  mdetuni0  21993  cpmadugsumlemB  22246  elptr2  22948  blss2ps  23779  blss2  23780  blssps  23800  blss  23801  xmeter  23809  metdcnlem  24222  lebnumii  24352  minveclem2  24813  pjthlem1  24824  volfiniun  24934  dvfsumrlimge0  25417  lgsdi  26705  cofcut1d  27269  ax5seglem3  27929  ax5seglem6  27932  axcontlem8  27969  eengtrkg  27984  vacn  29685  minvecolem2  29866  minvecolem4  29871  disjabrex  31553  disjabrexf  31554  2ndresdju  31618  fnpreimac  31640  slmdvs1  32111  slmd0vs  32115  orngsqr  32153  ornglmulle  32154  orngrmulle  32155  orngmullt  32158  suborng  32164  isprmidlc  32275  madjusmdetlem1  32472  cgrcomand  34629  cgrcomr  34635  cgrcomland  34637  cgrcomrand  34638  cgrtriv  34640  cgrid2  34641  ofscom  34645  cgrextend  34646  segconeq  34648  btwntriv2  34650  btwnexch3and  34659  btwnouttr2  34660  btwnouttr  34662  btwnexch  34663  btwnexchand  34664  btwndiff  34665  ifscgr  34682  cgrsub  34683  cgrxfr  34693  lineext  34714  endofsegid  34723  btwnconn1lem2  34726  btwnconn1lem3  34727  btwnconn1lem4  34728  btwnconn1lem5  34729  btwnconn1lem7  34731  btwnconn1lem8  34732  btwnconn1lem10  34734  btwnconn1lem11  34735  btwnconn1lem13  34737  btwnconn1lem14  34738  btwnconn3  34741  midofsegid  34742  segcon2  34743  brsegle2  34747  seglecgr12im  34748  seglecgr12  34749  seglerflx  34750  seglemin  34751  segletr  34752  btwnsegle  34755  colinbtwnle  34756  btwnoutside  34763  broutsideof3  34764  outsideoftr  34767  outsideofeq  34768  outsidele  34770  lineunray  34785  lineelsb2  34786  lfladdcl  37583  lshpkrlem4  37625  latmmdiN  37746  latmmdir  37747  hlatj4  37886  4atlem4b  38113  4atlem11  38122  4atlem12  38125  dalem2  38174  dalem-cly  38184  dalem10  38186  dalem23  38209  dalem38  38223  dalem44  38229  dalem55  38240  cdlema1N  38304  paddclN  38355  pmapjoin  38365  dalawlem3  38386  dalawlem5  38388  dalawlem7  38390  dalawlem8  38391  dalawlem11  38394  dalawlem12  38395  lhpexle3lem  38524  4atexlemc  38582  trlnidat  38686  arglem1N  38703  cdlemd9  38719  cdleme0moN  38738  cdleme11c  38774  cdleme11h  38779  cdleme11  38783  cdleme16c  38793  cdleme16f  38796  cdlemeda  38811  cdleme20l2  38834  cdlemefs32sn1aw  38927  cdleme43fsv1snlem  38933  cdleme41sn3a  38946  cdleme32fva  38950  cdleme32b  38955  cdleme32c  38956  cdleme32e  38958  cdleme40m  38980  cdleme40n  38981  cdleme42e  38992  cdleme48d  39048  cdlemf2  39075  cdlemf  39076  cdlemg2fv2  39113  cdlemg7fvbwN  39120  cdlemg7fvN  39137  cdlemg9a  39145  cdlemg9b  39146  cdlemg10a  39153  cdlemg12b  39157  cdlemg17b  39175  cdlemg31d  39213  cdlemg33b0  39214  cdlemg33a  39219  ltrnco  39232  ltrncom  39251  cdlemh  39330  cdlemk3  39346  cdlemk12  39363  cdlemk12u  39385  cdlemkfid1N  39434  cdlemk51  39466  cdlemk54  39471  cdlemk43N  39476  cdlemk35u  39477  cdlemk55u1  39478  cdlemk39u1  39480  cdlemk19u1  39482  dia2dimlem10  39586  dvhgrp  39620  dvh0g  39624  cdlemm10N  39631  diblsmopel  39684  cdlemn4  39711  cdlemn6  39715  cdlemn7  39716  dihordlem7  39727  dihord1  39731  dihord2pre  39738  dihvalcqat  39752  dihopelvalcpre  39761  dihord5apre  39775  dihord  39777  dih1  39799  dihglbcpreN  39813  dihjatc1  39824  dihmeetlem13N  39832  dihmeetALTN  39840  dihjatcclem1  39931  baerlem3lem1  40220  isdomn4  40674  pellfundex  41256  rmxypairf1o  41282  rmxycomplete  41288  rmxyneg  41291  rmxyadd  41292  rmxy1  41293  rmxy0  41294  jm2.22  41366  proot1mul  41573  deg1mhm  41581  stoweidlem7  44338  stoweidlem36  44367
  Copyright terms: Public domain W3C validator