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

Theorem syl122anc 1373
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 512 . 2 (𝜑 → (𝜏𝜂))
7 syl122anc.6 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl121anc 1369 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  divdiv32d  11433  divcan5d  11434  divcan7d  11436  divdiv1d  11439  divdiv2d  11440  seqcoll  13815  cau3lem  14707  eqsqrtd  14720  isercolllem2  15015  isercoll  15017  summolem2a  15064  divrcnv  15199  prodmolem2a  15280  prmind2  16021  divnumden  16080  pceulem  16174  pcqmul  16182  pcqdiv  16186  pcexp  16188  pcaddlem  16216  pcbc  16228  prmodvdslcmf  16375  latledi  17691  latjjdi  17705  latjjdir  17706  sylow1lem1  18645  sylow1lem5  18649  efgred2  18801  abladdsub4  18856  ablpnpcan  18862  ghmplusg  18888  frgpnabllem2  18916  isabvd  19513  lmodvs1  19584  lspsolvlem  19836  evlslem1  20215  frgpcyg  20638  ip2di  20703  mdetuni0  21148  cpmadugsumlemB  21400  elptr2  22100  blss2ps  22930  blss2  22931  blssps  22951  blss  22952  xmeter  22960  metdcnlem  23361  lebnumii  23487  minveclem2  23946  pjthlem1  23957  volfiniun  24065  dvfsumrlimge0  24544  lgsdi  25826  ax5seglem3  26633  ax5seglem6  26636  axcontlem8  26673  eengtrkg  26688  vacn  28387  minvecolem2  28568  minvecolem4  28573  disjabrex  30249  disjabrexf  30250  fnpreimac  30333  slmdvs1  30764  slmd0vs  30768  orngsqr  30793  ornglmulle  30794  orngrmulle  30795  orngmullt  30798  suborng  30804  isprmidlc  30870  madjusmdetlem1  30980  cgrcomand  33338  cgrcomr  33344  cgrcomland  33346  cgrcomrand  33347  cgrtriv  33349  cgrid2  33350  ofscom  33354  cgrextend  33355  segconeq  33357  btwntriv2  33359  btwnexch3and  33368  btwnouttr2  33369  btwnouttr  33371  btwnexch  33372  btwnexchand  33373  btwndiff  33374  ifscgr  33391  cgrsub  33392  cgrxfr  33402  lineext  33423  endofsegid  33432  btwnconn1lem2  33435  btwnconn1lem3  33436  btwnconn1lem4  33437  btwnconn1lem5  33438  btwnconn1lem7  33440  btwnconn1lem8  33441  btwnconn1lem10  33443  btwnconn1lem11  33444  btwnconn1lem13  33446  btwnconn1lem14  33447  btwnconn3  33450  midofsegid  33451  segcon2  33452  brsegle2  33456  seglecgr12im  33457  seglecgr12  33458  seglerflx  33459  seglemin  33460  segletr  33461  btwnsegle  33464  colinbtwnle  33465  btwnoutside  33472  broutsideof3  33473  outsideoftr  33476  outsideofeq  33477  outsidele  33479  lineunray  33494  lineelsb2  33495  lfladdcl  36076  lshpkrlem4  36118  latmmdiN  36239  latmmdir  36240  hlatj4  36379  4atlem4b  36605  4atlem11  36614  4atlem12  36617  dalem2  36666  dalem-cly  36676  dalem10  36678  dalem23  36701  dalem38  36715  dalem44  36721  dalem55  36732  cdlema1N  36796  paddclN  36847  pmapjoin  36857  dalawlem3  36878  dalawlem5  36880  dalawlem7  36882  dalawlem8  36883  dalawlem11  36886  dalawlem12  36887  lhpexle3lem  37016  4atexlemc  37074  trlnidat  37178  arglem1N  37195  cdlemd9  37211  cdleme0moN  37230  cdleme11c  37266  cdleme11h  37271  cdleme11  37275  cdleme16c  37285  cdleme16f  37288  cdlemeda  37303  cdleme20l2  37326  cdlemefs32sn1aw  37419  cdleme43fsv1snlem  37425  cdleme41sn3a  37438  cdleme32fva  37442  cdleme32b  37447  cdleme32c  37448  cdleme32e  37450  cdleme40m  37472  cdleme40n  37473  cdleme42e  37484  cdleme48d  37540  cdlemf2  37567  cdlemf  37568  cdlemg2fv2  37605  cdlemg7fvbwN  37612  cdlemg7fvN  37629  cdlemg9a  37637  cdlemg9b  37638  cdlemg10a  37645  cdlemg12b  37649  cdlemg17b  37667  cdlemg31d  37705  cdlemg33b0  37706  cdlemg33a  37711  ltrnco  37724  ltrncom  37743  cdlemh  37822  cdlemk3  37838  cdlemk12  37855  cdlemk12u  37877  cdlemkfid1N  37926  cdlemk51  37958  cdlemk54  37963  cdlemk43N  37968  cdlemk35u  37969  cdlemk55u1  37970  cdlemk39u1  37972  cdlemk19u1  37974  dia2dimlem10  38078  dvhgrp  38112  dvh0g  38116  cdlemm10N  38123  diblsmopel  38176  cdlemn4  38203  cdlemn6  38207  cdlemn7  38208  dihordlem7  38219  dihord1  38223  dihord2pre  38230  dihvalcqat  38244  dihopelvalcpre  38253  dihord5apre  38267  dihord  38269  dih1  38291  dihglbcpreN  38305  dihjatc1  38316  dihmeetlem13N  38324  dihmeetALTN  38332  dihjatcclem1  38423  baerlem3lem1  38712  pellfundex  39350  rmxypairf1o  39375  rmxycomplete  39381  rmxyneg  39384  rmxyadd  39385  rmxy1  39386  rmxy0  39387  jm2.22  39459  proot1mul  39666  deg1mhm  39674  stoweidlem7  42160  stoweidlem36  42189
  Copyright terms: Public domain W3C validator