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

Theorem syl122anc 1191
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
syl122anc.6  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
Assertion
Ref Expression
syl122anc  |-  ( ph  ->  ze )

Proof of Theorem syl122anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
64, 5jca 518 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl122anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl121anc 1187 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  divdiv32d  9577  divcan5d  9578  divcan7d  9580  divdiv1d  9583  divdiv2d  9584  seqcoll  11417  cau3lem  11854  eqsqrd  11867  isercolllem2  12155  isercoll  12157  summolem2a  12204  divrcnv  12327  prmind2  12785  divnumden  12835  pceulem  12914  pcqmul  12922  pcqdiv  12926  pcexp  12928  pcaddlem  12952  pcbc  12964  latledi  14211  latjjdi  14225  latjjdir  14226  sylow1lem1  14925  sylow1lem5  14929  efgred2  15078  abladdsub4  15131  ablpnpcan  15137  ghmplusg  15154  frgpnabllem2  15178  isabvd  15601  lmodvs1  15674  lspsolvlem  15911  frgpcyg  16543  ip2di  16561  elptr2  17285  qtophmeo  17524  blss2  17975  blss  17988  xmeter  17995  metdcnlem  18357  lebnumii  18480  minveclem2  18806  pjthlem1  18817  volfiniun  18920  dvfsumrlimge0  19393  evlslem1  19415  lgsdi  20587  gxdi  20979  vacn  21283  minvecolem2  21470  minvecolem4  21475  prodmolem2a  24157  ax5seglem3  24631  ax5seglem6  24634  axcontlem8  24671  cgrcomand  24686  cgrcomr  24692  cgrcomland  24694  cgrcomrand  24695  cgrtriv  24697  cgrid2  24698  ofscom  24702  cgrextend  24703  segconeq  24705  btwntriv2  24707  btwnexch3and  24716  btwnouttr2  24717  btwnouttr  24719  btwnexch  24720  btwnexchand  24721  btwndiff  24722  ifscgr  24739  cgrsub  24740  cgrxfr  24750  lineext  24771  endofsegid  24780  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem7  24788  btwnconn1lem8  24789  btwnconn1lem10  24791  btwnconn1lem11  24792  btwnconn1lem13  24794  btwnconn1lem14  24795  btwnconn3  24798  midofsegid  24799  segcon2  24800  brsegle2  24804  seglecgr12im  24805  seglecgr12  24806  seglerflx  24807  seglemin  24808  segletr  24809  btwnsegle  24812  colinbtwnle  24813  btwnoutside  24820  broutsideof3  24821  outsideoftr  24824  outsideofeq  24825  outsidele  24827  lineunray  24842  lineelsb2  24843  pellfundex  27074  rmxypairf1o  27099  rmxycomplete  27105  rmxyneg  27108  rmxyadd  27109  rmxy1  27110  rmxy0  27111  jm2.22  27191  proot1mul  27618  deg1mhm  27629  lfladdcl  29883  lshpkrlem4  29925  latmmdiN  30046  latmmdir  30047  hlatj4  30185  4atlem4b  30411  4atlem11  30420  4atlem12  30423  dalem2  30472  dalem-cly  30482  dalem10  30484  dalem23  30507  dalem38  30521  dalem44  30527  dalem55  30538  cdlema1N  30602  paddclN  30653  pmapjoin  30663  dalawlem3  30684  dalawlem5  30686  dalawlem7  30688  dalawlem8  30689  dalawlem11  30692  dalawlem12  30693  lhpexle3lem  30822  4atexlemc  30880  trlnidat  30984  arglem1N  31001  cdlemd9  31017  cdleme0moN  31036  cdleme11c  31072  cdleme11h  31077  cdleme11  31081  cdleme16c  31091  cdleme16f  31094  cdlemeda  31109  cdleme20l2  31132  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme41sn3a  31244  cdleme32fva  31248  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme40m  31278  cdleme40n  31279  cdleme42e  31290  cdleme48d  31346  cdlemf2  31373  cdlemf  31374  cdlemg2fv2  31411  cdlemg7fvbwN  31418  cdlemg7fvN  31435  cdlemg9a  31443  cdlemg9b  31444  cdlemg10a  31451  cdlemg12b  31455  cdlemg17b  31473  cdlemg31d  31511  cdlemg33b0  31512  cdlemg33a  31517  ltrnco  31530  ltrncom  31549  cdlemh  31628  cdlemk3  31644  cdlemk12  31661  cdlemk12u  31683  cdlemkfid1N  31732  cdlemk51  31764  cdlemk54  31769  cdlemk43N  31774  cdlemk35u  31775  cdlemk55u1  31776  cdlemk39u1  31778  cdlemk19u1  31780  dia2dimlem10  31885  dvhgrp  31919  dvh0g  31923  cdlemm10N  31930  diblsmopel  31983  cdlemn4  32010  cdlemn6  32014  cdlemn7  32015  dihordlem7  32026  dihord1  32030  dihord2pre  32037  dihvalcqat  32051  dihopelvalcpre  32060  dihord5apre  32074  dihord  32076  dih1  32098  dihglbcpreN  32112  dihjatc1  32123  dihmeetlem13N  32131  dihmeetALTN  32139  dihjatcclem1  32230  baerlem3lem1  32519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator