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  9561  divcan5d  9562  divcan7d  9564  divdiv1d  9567  divdiv2d  9568  seqcoll  11401  cau3lem  11838  eqsqrd  11851  isercolllem2  12139  isercoll  12141  summolem2a  12188  divrcnv  12311  prmind2  12769  divnumden  12819  pceulem  12898  pcqmul  12906  pcqdiv  12910  pcexp  12912  pcaddlem  12936  pcbc  12948  latledi  14195  latjjdi  14209  latjjdir  14210  sylow1lem1  14909  sylow1lem5  14913  efgred2  15062  abladdsub4  15115  ablpnpcan  15121  ghmplusg  15138  frgpnabllem2  15162  isabvd  15585  lmodvs1  15658  lspsolvlem  15895  frgpcyg  16527  ip2di  16545  elptr2  17269  qtophmeo  17508  blss2  17959  blss  17972  xmeter  17979  metdcnlem  18341  lebnumii  18464  minveclem2  18790  pjthlem1  18801  volfiniun  18904  dvfsumrlimge0  19377  evlslem1  19399  lgsdi  20571  gxdi  20963  vacn  21267  minvecolem2  21454  minvecolem4  21459  ax5seglem3  24559  ax5seglem6  24562  axcontlem8  24599  cgrcomand  24614  cgrcomr  24620  cgrcomland  24622  cgrcomrand  24623  cgrtriv  24625  cgrid2  24626  ofscom  24630  cgrextend  24631  segconeq  24633  btwntriv2  24635  btwnexch3and  24644  btwnouttr2  24645  btwnouttr  24647  btwnexch  24648  btwnexchand  24649  btwndiff  24650  ifscgr  24667  cgrsub  24668  cgrxfr  24678  lineext  24699  endofsegid  24708  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem7  24716  btwnconn1lem8  24717  btwnconn1lem10  24719  btwnconn1lem11  24720  btwnconn1lem13  24722  btwnconn1lem14  24723  btwnconn3  24726  midofsegid  24727  segcon2  24728  brsegle2  24732  seglecgr12im  24733  seglecgr12  24734  seglerflx  24735  seglemin  24736  segletr  24737  btwnsegle  24740  colinbtwnle  24741  btwnoutside  24748  broutsideof3  24749  outsideoftr  24752  outsideofeq  24753  outsidele  24755  lineunray  24770  lineelsb2  24771  pellfundex  26971  rmxypairf1o  26996  rmxycomplete  27002  rmxyneg  27005  rmxyadd  27006  rmxy1  27007  rmxy0  27008  jm2.22  27088  proot1mul  27515  deg1mhm  27526  lfladdcl  29261  lshpkrlem4  29303  latmmdiN  29424  latmmdir  29425  hlatj4  29563  4atlem4b  29789  4atlem11  29798  4atlem12  29801  dalem2  29850  dalem-cly  29860  dalem10  29862  dalem23  29885  dalem38  29899  dalem44  29905  dalem55  29916  cdlema1N  29980  paddclN  30031  pmapjoin  30041  dalawlem3  30062  dalawlem5  30064  dalawlem7  30066  dalawlem8  30067  dalawlem11  30070  dalawlem12  30071  lhpexle3lem  30200  4atexlemc  30258  trlnidat  30362  arglem1N  30379  cdlemd9  30395  cdleme0moN  30414  cdleme11c  30450  cdleme11h  30455  cdleme11  30459  cdleme16c  30469  cdleme16f  30472  cdlemeda  30487  cdleme20l2  30510  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme41sn3a  30622  cdleme32fva  30626  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme40m  30656  cdleme40n  30657  cdleme42e  30668  cdleme48d  30724  cdlemf2  30751  cdlemf  30752  cdlemg2fv2  30789  cdlemg7fvbwN  30796  cdlemg7fvN  30813  cdlemg9a  30821  cdlemg9b  30822  cdlemg10a  30829  cdlemg12b  30833  cdlemg17b  30851  cdlemg31d  30889  cdlemg33b0  30890  cdlemg33a  30895  ltrnco  30908  ltrncom  30927  cdlemh  31006  cdlemk3  31022  cdlemk12  31039  cdlemk12u  31061  cdlemkfid1N  31110  cdlemk51  31142  cdlemk54  31147  cdlemk43N  31152  cdlemk35u  31153  cdlemk55u1  31154  cdlemk39u1  31156  cdlemk19u1  31158  dia2dimlem10  31263  dvhgrp  31297  dvh0g  31301  cdlemm10N  31308  diblsmopel  31361  cdlemn4  31388  cdlemn6  31392  cdlemn7  31393  dihordlem7  31404  dihord1  31408  dihord2pre  31415  dihvalcqat  31429  dihopelvalcpre  31438  dihord5apre  31452  dihord  31454  dih1  31476  dihglbcpreN  31490  dihjatc1  31501  dihmeetlem13N  31509  dihmeetALTN  31517  dihjatcclem1  31608  baerlem3lem1  31897
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