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  5866  tfrlem1  6417  phplem4dom  6984  phplem4on  6990  fisseneq  7057  suplub2ti  7129  omp1eomlem  7222  nnnninfeq  7256  nninfisol  7261  exmidontriim  7368  addcmpblnq  7515  mulcmpblnq  7516  ordpipqqs  7522  ltexnqq  7556  enq0tr  7582  addcmpblnq0  7591  mulcmpblnq0  7592  nnnq0lem1  7594  prssnql  7627  prmuloc  7714  prmuloc2  7715  mullocpr  7719  ltexprlemopu  7751  ltexprlemrl  7758  ltexprlemru  7760  addcanprleml  7762  addcanprlemu  7763  ltmprr  7790  archpr  7791  suplocexprlemloc  7869  addcmpblnr  7887  mulcmpblnrlemg  7888  mulcmpblnr  7889  ltsrprg  7895  srpospr  7931  axcaucvglemres  8047  axpre-suploclemres  8049  axpre-suploc  8050  negeu  8298  add20  8582  rimul  8693  apreap  8695  cru  8710  mulge0  8727  mulap0  8762  prodgt0  8960  ltmul12a  8968  ledivdiv  8998  lediv12a  9002  qapne  9795  qreccl  9798  xleaddadd  10044  ixxss12  10063  ioodisj  10150  fznlem  10198  elfz0fzfz0  10283  btwnzge0  10480  seqf1og  10703  mulexpzap  10761  leexp1a  10776  expnbnd  10845  hashennnuni  10961  zfz1iso  11023  seq3coll  11024  swrdswrdlem  11195  pfxccatin12lem3  11223  resqrexlemga  11449  sqrtsq  11470  abs3lem  11537  cau3lem  11540  minmax  11656  xrmaxiflemval  11676  xrminmax  11691  climcau  11773  summodclem2  11808  fsumrelem  11897  cvgratz  11958  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  fprodcl2lem  12031  fprodap0  12047  fprodrec  12055  fprodap0f  12062  fprodle  12066  dvdsle  12270  bitsfzo  12381  bezoutlemmain  12434  bezoutlemzz  12438  dfgcd3  12446  dvdsmulgcd  12461  lcmcllem  12504  lcmgcdlem  12514  ncoprmgcdne1b  12526  qredeu  12534  oddpwdclemxy  12606  oddpwdclemdc  12610  pythagtriplem2  12704  pythagtrip  12721  pc2dvds  12768  pcz  12770  ctiunctlemfo  12925  unct  12928  sgrppropd  13360  mndpropd  13387  mhmeql  13439  mhmid  13566  mhmmnd  13567  mulgval  13573  issubg4m  13644  imasabl  13787  gsumfzconst  13792  reldvdsrsrg  13969  dvdsrmul1  13979  unitgrp  13993  neissex  14752  restbasg  14755  tgrest  14756  restopnb  14768  cnptopco  14809  metequiv2  15083  xmettx  15097  metcnpi3  15104  mpomulcn  15153  fsumcncntop  15154  elcncf2  15161  cncfmet  15179  dedekindeulemuub  15204  dedekindeulemlu  15208  dedekindicclemuub  15213  dedekindicclemlu  15217  limccnpcntop  15262  dvmptfsum  15312  reeff1olem  15358  lgsquad3  15676  nninfalllem1  16147  nninfnfiinf  16162  apdiff  16189