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  5818  tfrlem1  6363  phplem4dom  6920  phplem4on  6925  fisseneq  6990  suplub2ti  7062  omp1eomlem  7155  nnnninfeq  7189  nninfisol  7194  exmidontriim  7287  addcmpblnq  7429  mulcmpblnq  7430  ordpipqqs  7436  ltexnqq  7470  enq0tr  7496  addcmpblnq0  7505  mulcmpblnq0  7506  nnnq0lem1  7508  prssnql  7541  prmuloc  7628  prmuloc2  7629  mullocpr  7633  ltexprlemopu  7665  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  ltmprr  7704  archpr  7705  suplocexprlemloc  7783  addcmpblnr  7801  mulcmpblnrlemg  7802  mulcmpblnr  7803  ltsrprg  7809  srpospr  7845  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  negeu  8212  add20  8495  rimul  8606  apreap  8608  cru  8623  mulge0  8640  mulap0  8675  prodgt0  8873  ltmul12a  8881  ledivdiv  8911  lediv12a  8915  qapne  9707  qreccl  9710  xleaddadd  9956  ixxss12  9975  ioodisj  10062  fznlem  10110  elfz0fzfz0  10195  btwnzge0  10372  seqf1og  10595  mulexpzap  10653  leexp1a  10668  expnbnd  10737  hashennnuni  10853  zfz1iso  10915  seq3coll  10916  resqrexlemga  11170  sqrtsq  11191  abs3lem  11258  cau3lem  11261  minmax  11376  xrmaxiflemval  11396  xrminmax  11411  climcau  11493  summodclem2  11528  fsumrelem  11617  cvgratz  11678  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  fprodcl2lem  11751  fprodap0  11767  fprodrec  11775  fprodap0f  11782  fprodle  11786  dvdsle  11989  bezoutlemmain  12138  bezoutlemzz  12142  dfgcd3  12150  dvdsmulgcd  12165  lcmcllem  12208  lcmgcdlem  12218  ncoprmgcdne1b  12230  qredeu  12238  oddpwdclemxy  12310  oddpwdclemdc  12314  pythagtriplem2  12407  pythagtrip  12424  pc2dvds  12471  pcz  12473  ctiunctlemfo  12599  unct  12602  sgrppropd  12999  mndpropd  13024  mhmeql  13067  mhmid  13188  mhmmnd  13189  mulgval  13195  issubg4m  13266  imasabl  13409  gsumfzconst  13414  reldvdsrsrg  13591  dvdsrmul1  13601  unitgrp  13615  neissex  14344  restbasg  14347  tgrest  14348  restopnb  14360  cnptopco  14401  metequiv2  14675  xmettx  14689  metcnpi3  14696  mpomulcn  14745  fsumcncntop  14746  elcncf2  14753  cncfmet  14771  dedekindeulemuub  14796  dedekindeulemlu  14800  dedekindicclemuub  14805  dedekindicclemlu  14809  limccnpcntop  14854  dvmptfsum  14904  reeff1olem  14947  lgsquad3  15241  nninfalllem1  15568  apdiff  15608