Theorem syl112anc 1330

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.4	|- ( ph -> ta )
syl112anc.5	|- ( ( ps /\ ch /\ ( th /\ ta ) ) -> et )

Assertion

Ref	Expression
syl112anc	|- ( ph -> et )

Proof of Theorem syl112anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. 2 |- ( ph -> ch )
3		syl12anc.3	. . 3 |- ( ph -> th )
4		syl22anc.4	. . 3 |- ( ph -> ta )
5	3, 4	jca 554	. 2 |- ( ph -> ( th /\ ta ) )
6		syl112anc.5	. 2 |- ( ( ps /\ ch /\ ( th /\ ta ) ) -> et )
7	1, 2, 5, 6	syl3anc 1326	1 |- ( ph -> et )

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:  rmob2  3531  fveqf1o  6557  enfixsn  8069  gruina  9640  grur1  9642  enqeq  9756  recrec  10722  rec11r  10724  divdivdiv  10726  dmdcan  10735  ddcan  10739  rereccl  10743  div2neg  10748  divmuld  10823  divmul2d  10834  divmul3d  10835  divassd  10836  div12d  10837  div23d  10838  divdird  10839  divsubdird  10840  div11d  10841  ltmul12a  10879  ltdiv1  10887  ltrec  10905  lt2msq1  10907  lediv2  10913  supmul1  10992  qbtwnre  12030  xlemul1a  12118  xlemul1  12120  xadd4d  12133  quoremz  12654  quoremnn0ALT  12656  expgt1  12898  nnlesq  12968  expnbnd  12993  expmulnbnd  12996  discr1  13000  facubnd  13087  hashf1lem1  13239  2swrdeqwrdeq  13453  sqrlem6  13988  mulcn2  14326  climcnds  14583  geomulcvg  14607  cvgrat  14615  eftlub  14839  eflegeo  14851  tanhlt1  14890  sin01bnd  14915  cos01bnd  14916  eirrlem  14932  bitsmod  15158  mulgcd  15265  mulgcddvds  15369  prmind2  15398  qnumgt0  15458  iserodd  15540  pcpremul  15548  fldivp1  15601  pcfaclem  15602  qexpz  15605  prmpwdvds  15608  pockthg  15610  prmreclem1  15620  prmreclem5  15624  4sqlem10  15651  4sqlem12  15660  4sqlem16  15664  4sqlem17  15665  vdwlem3  15687  vdwlem8  15692  vdwlem9  15693  0ram  15724  ramz2  15728  xpsc0  16220  xpsc1  16221  odmulg  17973  dfod2  17981  odf1o1  17987  odf1o2  17988  sylow3lem4  18045  ablsub4  18218  odadd1  18251  odadd2  18252  ablfacrp2  18466  ablfac1b  18469  ablfac1eu  18472  pgpfac1lem3a  18475  pgpfaclem2  18481  chrcong  19877  znrrg  19914  cygznlem1  19915  chpdmatlem3  20645  txdis  21435  txdis1cn  21438  ptunhmeo  21611  qustgplem  21924  blcld  22310  nlmvscnlem2  22489  blcvx  22601  metds0  22653  metdseq0  22657  icopnfcnv  22741  lebnumii  22765  ipcau2  23033  tchcphlem1  23034  ipcnlem2  23043  csbren  23182  trirn  23183  dyadf  23359  dyadovol  23361  dyaddisjlem  23363  dyadmaxlem  23365  opnmbllem  23369  mbfmulc2lem  23414  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2mulclem  23513  itg2monolem1  23517  itg2monolem3  23519  itg2cnlem2  23529  itgabs  23601  dvlip  23756  dvlt0  23768  dvcvx  23783  ftc1lem4  23802  dgrcolem2  24030  aaliou3lem2  24098  aaliou3lem9  24105  itgulm  24162  radcnvlem1  24167  abelthlem2  24186  abelthlem7  24192  tangtx  24257  cosne0  24276  cosordlem  24277  tanord1  24283  logdivlti  24366  logcnlem4  24391  logf1o2  24396  cxpcn3lem  24488  cxpaddle  24493  ang180lem2  24540  atanlogsublem  24642  atantan  24650  atanbndlem  24652  atans2  24658  leibpi  24669  log2tlbnd  24672  birthdaylem3  24680  efrlim  24696  jensenlem2  24714  zetacvg  24741  ftalem1  24799  ftalem5  24803  basellem1  24807  basellem4  24810  fsumdvdsdiaglem  24909  dvdsflf1o  24913  fsumfldivdiaglem  24915  ppiub  24929  mersenne  24952  dchrptlem1  24989  bposlem1  25009  bposlem2  25010  bposlem4  25012  lgsdilem  25049  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgsquadlem1  25105  lgsquadlem2  25106  2sqlem3  25145  2sqlem8  25151  2sqlem11  25154  2sqblem  25156  chebbnd1lem2  25159  chebbnd1lem3  25160  rplogsumlem1  25173  rplogsumlem2  25174  dchrisumlem1  25178  dchrmusum2  25183  dchrisum0flblem1  25197  mulog2sumlem1  25223  logdivbnd  25245  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntlemh  25288  pntlemr  25291  pntlemk  25295  pntlemo  25296  ostth2lem1  25307  ostth2lem2  25323  ostth2lem3  25324  ostth3  25327  legov  25480  axsegcon  25807  axpaschlem  25820  0uhgrsubgr  26171  clwwlksf1  26917  upgr4cycl4dv4e  27045  eupth2lem3lem3  27090  nmblolbii  27654  nmbdoplbi  28883  nmcoplbi  28887  nmophmi  28890  nmbdfnlbi  28908  nmcfnlbi  28911  cnlnadjlem7  28932  nmopcoi  28954  resf1o  29505  xdivrec  29635  txomap  29901  unitdivcld  29947  measvunilem  30275  measvuni  30277  measssd  30278  measiuns  30280  measinblem  30283  measdivcst  30288  sibfof  30402  oddpwdc  30416  sseqfv1  30451  sseqfv2  30456  probun  30481  totprobd  30488  dstrvprob  30533  actfunsnrndisj  30683  reprsuc  30693  breprexplema  30708  subfaclim  31170  connpconn  31217  cvmliftlem2  31268  cvmliftlem6  31272  cvmliftlem7  31273  cvmliftlem8  31274  cvmliftlem9  31275  cvmliftlem10  31276  snmlff  31311  noextenddif  31821  noextendlt  31822  noextendgt  31823  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd1lem6  31859  noetalem3  31865  lineext  32183  hilbert1.1  32261  nn0prpwlem  32317  poimirlem1  33410  opnmbllem0  33445  ismblfin  33450  itgabsnc  33479  ftc1cnnclem  33483  bfplem1  33621  bfp  33623  lfl1  34357  lfladdcl  34358  eqlkr  34386  lkrlsp  34389  atcvrj2b  34718  3dim1  34753  3dim2  34754  llni2  34798  2llnjaN  34852  lvoli3  34863  lvoli2  34867  lncvrelatN  35067  lhpat4N  35330  lhpat3  35332  4atexlemex6  35360  ldilco  35402  ltrnid  35421  ltrnatb  35423  ltrnel  35425  ltrncnvel  35428  ltrncnv  35432  ltrn11at  35433  ltrneq  35435  ltrnmwOLD  35438  trlat  35456  trlator0  35458  ltrnnidn  35461  trlid0  35463  trlnidatb  35464  trlnle  35473  trlval3  35474  trlval4  35475  cdlemc2  35479  cdlemc5  35482  cdlemc6  35483  cdlemc  35484  cdlemd2  35486  cdlemd9  35493  cdleme0e  35504  cdleme02N  35509  cdleme0ex1N  35510  cdleme3e  35519  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme7aa  35529  cdleme7b  35531  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme9  35540  cdleme16aN  35546  cdleme11c  35548  cdleme11dN  35549  cdleme11e  35550  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme12  35558  cdleme21j  35624  cdleme26eALTN  35649  cdleme26f  35651  cdleme26f2  35653  cdlemefrs29bpre0  35684  cdleme35a  35736  cdleme35b  35738  cdleme35c  35739  cdleme35f  35742  cdleme36a  35748  cdleme38m  35751  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemf  35851  cdlemg2fvlem  35882  cdlemg2l  35891  cdlemg7N  35914  cdlemg12g  35937  cdlemg15  35944  cdlemg17h  35956  cdlemg17  35965  cdlemg19a  35971  cdlemg24  35976  cdlemg37  35977  cdlemg27a  35980  cdlemg31b0N  35982  cdlemg27b  35984  cdlemg31c  35987  cdlemg31d  35988  cdlemg35  36001  trljco  36028  tgrpgrplem  36037  cdlemh2  36104  tendoconid  36117  tendotr  36118  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk53b  36244  cdlemk53  36245  cdlemk54  36246  cdleml3N  36266  cdleml5N  36268  tendospcanN  36312  diclss  36482  dihvalcq2  36536  dihord4  36547  dihord5b  36548  dihord5apre  36551  dihmeetlem1N  36579  dihmeetbclemN  36593  dihmeetlem20N  36615  dihmeetALTN  36616  dihatlat  36623  dihatexv  36627  dochkr1  36767  dochkr1OLDN  36768  lcfl7lem  36788  lclkrlem2m  36808  hdmaplna1  37199  hdmaplns1  37200  hdmaplnm1  37201  eldioph2lem1  37323  fphpdo  37381  irrapxlem1  37386  irrapxlem2  37387  irrapxlem3  37388  irrapxlem5  37390  pellexlem2  37394  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell1234qrdich  37425  pell1qr1  37435  pellqrexplicit  37441  pellfundex  37450  reglogltb  37455  reglogleb  37456  pellfund14  37462  rmspecsqrtnqOLD  37471  rmxycomplete  37482  jm2.24nn  37526  jm2.17b  37528  jm2.17c  37529  jm2.18  37555  jm2.19lem2  37557  jm2.20nn  37564  jm2.16nn0  37571  jm3.1lem2  37585  areaquad  37802  clsk3nimkb  38338  lemuldiv3d  38472  lemuldiv4d  38473  stoweidlem1  40218  stoweidlem11  40228  stoweidlem14  40231  stoweidlem26  40243  stoweidlem34  40251  stoweidlem38  40255  stoweidlem60  40277  fourierdlem52  40375  etransclem38  40489  pfxsuffeqwrdeq  41406  domnmsuppn0  42150  lincvalpr  42207  ldepspr  42262  islindeps2  42272  fldivexpfllog2  42359