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

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

Proof of Theorem syl122anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 552 . 2 (𝜑 → (𝜏𝜂))
7 syl122anc.6 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl121anc 1322 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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  df-3an 1032
This theorem is referenced by:  divdiv32d  10672  divcan5d  10673  divcan7d  10675  divdiv1d  10678  divdiv2d  10679  seqcoll  13054  cau3lem  13885  eqsqrtd  13898  isercolllem2  14187  isercoll  14189  summolem2a  14236  divrcnv  14366  prodmolem2a  14446  prmind2  15179  divnumden  15237  pceulem  15331  pcqmul  15339  pcqdiv  15343  pcexp  15345  pcaddlem  15373  pcbc  15385  prmodvdslcmf  15532  latledi  16855  latjjdi  16869  latjjdir  16870  sylow1lem1  17779  sylow1lem5  17783  efgred2  17932  abladdsub4  17985  ablpnpcan  17991  ghmplusg  18015  frgpnabllem2  18043  isabvd  18586  lmodvs1  18657  lspsolvlem  18906  evlslem1  19279  frgpcyg  19683  ip2di  19747  mdetuni0  20185  cpmadugsumlemB  20437  elptr2  21126  blss2ps  21956  blss2  21957  blssps  21977  blss  21978  xmeter  21986  metdcnlem  22376  lebnumii  22501  minveclem2  22919  pjthlem1  22930  volfiniun  23036  dvfsumrlimge0  23511  lgsdi  24773  ax5seglem3  25526  ax5seglem6  25529  axcontlem8  25566  eengtrkg  25580  vacn  26731  minvecolem2  26918  minvecolem4  26923  disjabrex  28580  disjabrexf  28581  slmdvs1  28907  slmd0vs  28911  orngsqr  28938  ornglmulle  28939  orngrmulle  28940  orngmullt  28943  suborng  28949  madjusmdetlem1  29024  cgrcomand  31071  cgrcomr  31077  cgrcomland  31079  cgrcomrand  31080  cgrtriv  31082  cgrid2  31083  ofscom  31087  cgrextend  31088  segconeq  31090  btwntriv2  31092  btwnexch3and  31101  btwnouttr2  31102  btwnouttr  31104  btwnexch  31105  btwnexchand  31106  btwndiff  31107  ifscgr  31124  cgrsub  31125  cgrxfr  31135  lineext  31156  endofsegid  31165  btwnconn1lem2  31168  btwnconn1lem3  31169  btwnconn1lem4  31170  btwnconn1lem5  31171  btwnconn1lem7  31173  btwnconn1lem8  31174  btwnconn1lem10  31176  btwnconn1lem11  31177  btwnconn1lem13  31179  btwnconn1lem14  31180  btwnconn3  31183  midofsegid  31184  segcon2  31185  brsegle2  31189  seglecgr12im  31190  seglecgr12  31191  seglerflx  31192  seglemin  31193  segletr  31194  btwnsegle  31197  colinbtwnle  31198  btwnoutside  31205  broutsideof3  31206  outsideoftr  31209  outsideofeq  31210  outsidele  31212  lineunray  31227  lineelsb2  31228  lfladdcl  33176  lshpkrlem4  33218  latmmdiN  33339  latmmdir  33340  hlatj4  33478  4atlem4b  33704  4atlem11  33713  4atlem12  33716  dalem2  33765  dalem-cly  33775  dalem10  33777  dalem23  33800  dalem38  33814  dalem44  33820  dalem55  33831  cdlema1N  33895  paddclN  33946  pmapjoin  33956  dalawlem3  33977  dalawlem5  33979  dalawlem7  33981  dalawlem8  33982  dalawlem11  33985  dalawlem12  33986  lhpexle3lem  34115  4atexlemc  34173  trlnidat  34278  arglem1N  34295  cdlemd9  34311  cdleme0moN  34330  cdleme11c  34366  cdleme11h  34371  cdleme11  34375  cdleme16c  34385  cdleme16f  34388  cdlemeda  34403  cdleme20l2  34427  cdlemefs32sn1aw  34520  cdleme43fsv1snlem  34526  cdleme41sn3a  34539  cdleme32fva  34543  cdleme32b  34548  cdleme32c  34549  cdleme32e  34551  cdleme40m  34573  cdleme40n  34574  cdleme42e  34585  cdleme48d  34641  cdlemf2  34668  cdlemf  34669  cdlemg2fv2  34706  cdlemg7fvbwN  34713  cdlemg7fvN  34730  cdlemg9a  34738  cdlemg9b  34739  cdlemg10a  34746  cdlemg12b  34750  cdlemg17b  34768  cdlemg31d  34806  cdlemg33b0  34807  cdlemg33a  34812  ltrnco  34825  ltrncom  34844  cdlemh  34923  cdlemk3  34939  cdlemk12  34956  cdlemk12u  34978  cdlemkfid1N  35027  cdlemk51  35059  cdlemk54  35064  cdlemk43N  35069  cdlemk35u  35070  cdlemk55u1  35071  cdlemk39u1  35073  cdlemk19u1  35075  dia2dimlem10  35180  dvhgrp  35214  dvh0g  35218  cdlemm10N  35225  diblsmopel  35278  cdlemn4  35305  cdlemn6  35309  cdlemn7  35310  dihordlem7  35321  dihord1  35325  dihord2pre  35332  dihvalcqat  35346  dihopelvalcpre  35355  dihord5apre  35369  dihord  35371  dih1  35393  dihglbcpreN  35407  dihjatc1  35418  dihmeetlem13N  35426  dihmeetALTN  35434  dihjatcclem1  35525  baerlem3lem1  35814  pellfundex  36268  rmxypairf1o  36294  rmxycomplete  36300  rmxyneg  36303  rmxyadd  36304  rmxy1  36305  rmxy0  36306  jm2.22  36380  proot1mul  36596  deg1mhm  36604  stoweidlem7  38701  stoweidlem36  38730
  Copyright terms: Public domain W3C validator