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  5980  suppcofn  6506  tfrlem1  6579  phplem4dom  7163  phplem4on  7169  fisseneq  7242  suplub2ti  7342  omp1eomlem  7435  nnnninfeq  7469  nninfisol  7474  exmidontriim  7582  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  ltexnqq  7776  enq0tr  7802  addcmpblnq0  7811  mulcmpblnq0  7812  nnnq0lem1  7814  prssnql  7847  prmuloc  7934  prmuloc2  7935  mullocpr  7939  ltexprlemopu  7971  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  ltmprr  8010  archpr  8011  suplocexprlemloc  8089  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  ltsrprg  8115  srpospr  8151  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  negeu  8519  add20  8804  rimul  8916  apreap  8918  cru  8933  mulge0  8950  mulap0  8985  prodgt0  9185  ltmul12a  9193  ledivdiv  9223  lediv12a  9227  qapne  10049  qreccl  10052  irraddap  10057  xleaddadd  10300  ixxss12  10319  ioodisj  10406  fznlem  10456  elfz0fzfz0  10544  btwnzge0  10750  seqf1og  10973  mulexpzap  11031  leexp1a  11046  expnbnd  11116  hashennnuni  11234  hashf1lem2  11302  zfz1iso  11309  seq3coll  11310  swrdswrdlem  11492  pfxccatin12lem3  11520  resqrexlemga  11805  sqrtsq  11826  abs3lem  11894  cau3lem  11897  minmax  12014  xrmaxiflemval  12035  xrminmax  12050  climcau  12132  summodclem2  12168  fsumrelem  12257  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  fprodcl2lem  12391  fprodap0  12407  fprodrec  12415  fprodap0f  12422  fprodle  12426  dvdsle  12630  bitsfzo  12741  bezoutlemmain  12794  bezoutlemzz  12798  dfgcd3  12806  dvdsmulgcd  12821  lcmcllem  12864  lcmgcdlem  12874  ncoprmgcdne1b  12886  qredeu  12894  pwbdvdseu  12966  nnmaxpwlemparts  12971  pythagtriplem2  13068  pythagtrip  13085  pc2dvds  13132  pcz  13134  ctiunctlemfo  13382  unct  13385  sgrppropd  13781  mndpropd  13806  mhmeql  13852  mhmid  13971  mhmmnd  13972  mulgval  13978  issubg4m  14049  imasabl  14224  gzsumconst  14227  gsumzfi  14242  gsummptfidmadd  14245  dvdsrmul1  14493  unitgrp  14507  aprlring  14684  gsumfsum  15007  issubassa2  15119  neissex  15357  restbasg  15360  tgrest  15361  restopnb  15373  cnptopco  15414  metequiv2  15688  xmettx  15702  metcnpi3  15709  mpomulcn  15758  fsumcncntop  15759  elcncf2  15766  cncfmet  15784  dedekindeulemuub  15809  dedekindeulemlu  15813  dedekindicclemuub  15818  dedekindicclemlu  15822  limccnpcntop  15867  dvmptfsum  15917  reeff1olem  15963  lgsquad3  16369  clwwlkccatlem  16807  nninfalllem1  17217  nninfnfiinf  17232  apdiff  17264