Theorem simplll 533

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 488	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp-4l  541  f1imass  5843  tfrlem1  6394  phplem4dom  6959  phplem4on  6964  fisseneq  7031  suplub2ti  7103  omp1eomlem  7196  nnnninfeq  7230  nninfisol  7235  exmidontriim  7337  addcmpblnq  7480  mulcmpblnq  7481  ordpipqqs  7487  ltexnqq  7521  enq0tr  7547  addcmpblnq0  7556  mulcmpblnq0  7557  nnnq0lem1  7559  prssnql  7592  prmuloc  7679  prmuloc2  7680  mullocpr  7684  ltexprlemopu  7716  ltexprlemrl  7723  ltexprlemru  7725  addcanprleml  7727  addcanprlemu  7728  ltmprr  7755  archpr  7756  suplocexprlemloc  7834  addcmpblnr  7852  mulcmpblnrlemg  7853  mulcmpblnr  7854  ltsrprg  7860  srpospr  7896  axcaucvglemres  8012  axpre-suploclemres  8014  axpre-suploc  8015  negeu  8263  add20  8547  rimul  8658  apreap  8660  cru  8675  mulge0  8692  mulap0  8727  prodgt0  8925  ltmul12a  8933  ledivdiv  8963  lediv12a  8967  qapne  9760  qreccl  9763  xleaddadd  10009  ixxss12  10028  ioodisj  10115  fznlem  10163  elfz0fzfz0  10248  btwnzge0  10443  seqf1og  10666  mulexpzap  10724  leexp1a  10739  expnbnd  10808  hashennnuni  10924  zfz1iso  10986  seq3coll  10987  resqrexlemga  11334  sqrtsq  11355  abs3lem  11422  cau3lem  11425  minmax  11541  xrmaxiflemval  11561  xrminmax  11576  climcau  11658  summodclem2  11693  fsumrelem  11782  cvgratz  11843  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  fprodcl2lem  11916  fprodap0  11932  fprodrec  11940  fprodap0f  11947  fprodle  11951  dvdsle  12155  bitsfzo  12266  bezoutlemmain  12319  bezoutlemzz  12323  dfgcd3  12331  dvdsmulgcd  12346  lcmcllem  12389  lcmgcdlem  12399  ncoprmgcdne1b  12411  qredeu  12419  oddpwdclemxy  12491  oddpwdclemdc  12495  pythagtriplem2  12589  pythagtrip  12606  pc2dvds  12653  pcz  12655  ctiunctlemfo  12810  unct  12813  sgrppropd  13245  mndpropd  13272  mhmeql  13324  mhmid  13451  mhmmnd  13452  mulgval  13458  issubg4m  13529  imasabl  13672  gsumfzconst  13677  reldvdsrsrg  13854  dvdsrmul1  13864  unitgrp  13878  neissex  14637  restbasg  14640  tgrest  14641  restopnb  14653  cnptopco  14694  metequiv2  14968  xmettx  14982  metcnpi3  14989  mpomulcn  15038  fsumcncntop  15039  elcncf2  15046  cncfmet  15064  dedekindeulemuub  15089  dedekindeulemlu  15093  dedekindicclemuub  15098  dedekindicclemlu  15102  limccnpcntop  15147  dvmptfsum  15197  reeff1olem  15243  lgsquad3  15561  nninfalllem1  15945  nninfnfiinf  15960  apdiff  15987