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

Theorem syl122anc 1334
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 554 . 2 (𝜑 → (𝜏𝜂))
7 syl122anc.6 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl121anc 1330 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037
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 197  df-an 386  df-3an 1039
This theorem is referenced by:  divdiv32d  10823  divcan5d  10824  divcan7d  10826  divdiv1d  10829  divdiv2d  10830  seqcoll  13243  cau3lem  14088  eqsqrtd  14101  isercolllem2  14390  isercoll  14392  summolem2a  14440  divrcnv  14578  prodmolem2a  14658  prmind2  15392  divnumden  15450  pceulem  15544  pcqmul  15552  pcqdiv  15556  pcexp  15558  pcaddlem  15586  pcbc  15598  prmodvdslcmf  15745  latledi  17083  latjjdi  17097  latjjdir  17098  sylow1lem1  18007  sylow1lem5  18011  efgred2  18160  abladdsub4  18213  ablpnpcan  18219  ghmplusg  18243  frgpnabllem2  18271  isabvd  18814  lmodvs1  18885  lspsolvlem  19136  evlslem1  19509  frgpcyg  19916  ip2di  19980  mdetuni0  20421  cpmadugsumlemB  20673  elptr2  21371  blss2ps  22202  blss2  22203  blssps  22223  blss  22224  xmeter  22232  metdcnlem  22633  lebnumii  22759  minveclem2  23191  pjthlem1  23202  volfiniun  23309  dvfsumrlimge0  23787  lgsdi  25053  ax5seglem3  25805  ax5seglem6  25808  axcontlem8  25845  eengtrkg  25859  vacn  27533  minvecolem2  27715  minvecolem4  27720  disjabrex  29379  disjabrexf  29380  slmdvs1  29758  slmd0vs  29762  orngsqr  29789  ornglmulle  29790  orngrmulle  29791  orngmullt  29794  suborng  29800  madjusmdetlem1  29878  cgrcomand  32082  cgrcomr  32088  cgrcomland  32090  cgrcomrand  32091  cgrtriv  32093  cgrid2  32094  ofscom  32098  cgrextend  32099  segconeq  32101  btwntriv2  32103  btwnexch3and  32112  btwnouttr2  32113  btwnouttr  32115  btwnexch  32116  btwnexchand  32117  btwndiff  32118  ifscgr  32135  cgrsub  32136  cgrxfr  32146  lineext  32167  endofsegid  32176  btwnconn1lem2  32179  btwnconn1lem3  32180  btwnconn1lem4  32181  btwnconn1lem5  32182  btwnconn1lem7  32184  btwnconn1lem8  32185  btwnconn1lem10  32187  btwnconn1lem11  32188  btwnconn1lem13  32190  btwnconn1lem14  32191  btwnconn3  32194  midofsegid  32195  segcon2  32196  brsegle2  32200  seglecgr12im  32201  seglecgr12  32202  seglerflx  32203  seglemin  32204  segletr  32205  btwnsegle  32208  colinbtwnle  32209  btwnoutside  32216  broutsideof3  32217  outsideoftr  32220  outsideofeq  32221  outsidele  32223  lineunray  32238  lineelsb2  32239  lfladdcl  34184  lshpkrlem4  34226  latmmdiN  34347  latmmdir  34348  hlatj4  34486  4atlem4b  34712  4atlem11  34721  4atlem12  34724  dalem2  34773  dalem-cly  34783  dalem10  34785  dalem23  34808  dalem38  34822  dalem44  34828  dalem55  34839  cdlema1N  34903  paddclN  34954  pmapjoin  34964  dalawlem3  34985  dalawlem5  34987  dalawlem7  34989  dalawlem8  34990  dalawlem11  34993  dalawlem12  34994  lhpexle3lem  35123  4atexlemc  35181  trlnidat  35286  arglem1N  35303  cdlemd9  35319  cdleme0moN  35338  cdleme11c  35374  cdleme11h  35379  cdleme11  35383  cdleme16c  35393  cdleme16f  35396  cdlemeda  35411  cdleme20l2  35435  cdlemefs32sn1aw  35528  cdleme43fsv1snlem  35534  cdleme41sn3a  35547  cdleme32fva  35551  cdleme32b  35556  cdleme32c  35557  cdleme32e  35559  cdleme40m  35581  cdleme40n  35582  cdleme42e  35593  cdleme48d  35649  cdlemf2  35676  cdlemf  35677  cdlemg2fv2  35714  cdlemg7fvbwN  35721  cdlemg7fvN  35738  cdlemg9a  35746  cdlemg9b  35747  cdlemg10a  35754  cdlemg12b  35758  cdlemg17b  35776  cdlemg31d  35814  cdlemg33b0  35815  cdlemg33a  35820  ltrnco  35833  ltrncom  35852  cdlemh  35931  cdlemk3  35947  cdlemk12  35964  cdlemk12u  35986  cdlemkfid1N  36035  cdlemk51  36067  cdlemk54  36072  cdlemk43N  36077  cdlemk35u  36078  cdlemk55u1  36079  cdlemk39u1  36081  cdlemk19u1  36083  dia2dimlem10  36188  dvhgrp  36222  dvh0g  36226  cdlemm10N  36233  diblsmopel  36286  cdlemn4  36313  cdlemn6  36317  cdlemn7  36318  dihordlem7  36329  dihord1  36333  dihord2pre  36340  dihvalcqat  36354  dihopelvalcpre  36363  dihord5apre  36377  dihord  36379  dih1  36401  dihglbcpreN  36415  dihjatc1  36426  dihmeetlem13N  36434  dihmeetALTN  36442  dihjatcclem1  36533  baerlem3lem1  36822  pellfundex  37276  rmxypairf1o  37302  rmxycomplete  37308  rmxyneg  37311  rmxyadd  37312  rmxy1  37313  rmxy0  37314  jm2.22  37388  proot1mul  37603  deg1mhm  37611  stoweidlem7  39993  stoweidlem36  40022
  Copyright terms: Public domain W3C validator