Theorem simplll 539

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplll	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )

Proof of Theorem simplll

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	ad2antrr 492	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-4l  547  f1imass  5983  suppcofn  6510  tfrlem1  6583  phplem4dom  7167  phplem4on  7173  fisseneq  7246  suplub2ti  7347  omp1eomlem  7440  nnnninfeq  7474  nninfisol  7479  exmidontriim  7587  addcmpblnq  7740  mulcmpblnq  7741  ordpipqqs  7747  ltexnqq  7781  enq0tr  7807  addcmpblnq0  7816  mulcmpblnq0  7817  nnnq0lem1  7819  prssnql  7852  prmuloc  7939  prmuloc2  7940  mullocpr  7944  ltexprlemopu  7976  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  ltmprr  8015  archpr  8016  suplocexprlemloc  8094  addcmpblnr  8112  mulcmpblnrlemg  8113  mulcmpblnr  8114  ltsrprg  8120  srpospr  8156  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  negeu  8524  add20  8809  rimul  8921  apreap  8923  cru  8938  mulge0  8955  mulap0  8990  prodgt0  9190  ltmul12a  9198  ledivdiv  9228  lediv12a  9232  qapne  10055  qreccl  10058  irraddap  10063  xleaddadd  10306  ixxss12  10325  ioodisj  10412  fznlem  10462  elfz0fzfz0  10550  btwnzge0  10756  seqf1og  10979  mulexpzap  11037  leexp1a  11052  expnbnd  11122  hashennnuni  11240  hashf1lem2  11308  zfz1iso  11315  seq3coll  11316  swrdswrdlem  11498  pfxccatin12lem3  11526  resqrexlemga  11811  sqrtsq  11832  abs3lem  11900  cau3lem  11903  minmax  12020  xrmaxiflemval  12041  xrminmax  12056  climcau  12138  summodclem2  12174  fsumrelem  12263  cvgratz  12324  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  fprodcl2lem  12397  fprodap0  12413  fprodrec  12421  fprodap0f  12428  fprodle  12432  dvdsle  12636  bitsfzo  12747  bezoutlemmain  12800  bezoutlemzz  12804  dfgcd3  12812  dvdsmulgcd  12827  lcmcllem  12870  lcmgcdlem  12880  ncoprmgcdne1b  12892  qredeu  12900  pwbdvdseu  12972  nnmaxpwlemparts  12977  pythagtriplem2  13074  pythagtrip  13091  pc2dvds  13138  pcz  13140  ctiunctlemfo  13388  unct  13391  sgrppropd  13787  mndpropd  13812  mhmeql  13858  mhmid  13977  mhmmnd  13978  mulgval  13984  issubg4m  14055  imasabl  14230  gzsumconst  14233  gsumzfi  14248  gsummptfidmadd  14251  gsummptfidmsplit  14254  dvdsrmul1  14518  unitgrp  14532  aprlring  14709  gsumfsum  15032  issubassa2  15144  neissex  15391  restbasg  15394  tgrest  15395  restopnb  15407  cnptopco  15448  metequiv2  15722  xmettx  15736  metcnpi3  15743  mpomulcn  15792  fsumcncntop  15793  elcncf2  15800  cncfmet  15818  dedekindeulemuub  15843  dedekindeulemlu  15847  dedekindicclemuub  15852  dedekindicclemlu  15856  limccnpcntop  15901  dvmptfsum  15951  reeff1olem  15997  lgsquad3  16408  clwwlkccatlem  16846  nninfalllem1  17257  nninfnfiinf  17272  apdiff  17304