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  5795  tfrlem1  6332  phplem4dom  6889  phplem4on  6894  fisseneq  6959  suplub2ti  7029  omp1eomlem  7122  nnnninfeq  7155  nninfisol  7160  exmidontriim  7253  addcmpblnq  7395  mulcmpblnq  7396  ordpipqqs  7402  ltexnqq  7436  enq0tr  7462  addcmpblnq0  7471  mulcmpblnq0  7472  nnnq0lem1  7474  prssnql  7507  prmuloc  7594  prmuloc2  7595  mullocpr  7599  ltexprlemopu  7631  ltexprlemrl  7638  ltexprlemru  7640  addcanprleml  7642  addcanprlemu  7643  ltmprr  7670  archpr  7671  suplocexprlemloc  7749  addcmpblnr  7767  mulcmpblnrlemg  7768  mulcmpblnr  7769  ltsrprg  7775  srpospr  7811  axcaucvglemres  7927  axpre-suploclemres  7929  axpre-suploc  7930  negeu  8177  add20  8460  rimul  8571  apreap  8573  cru  8588  mulge0  8605  mulap0  8640  prodgt0  8838  ltmul12a  8846  ledivdiv  8876  lediv12a  8880  qapne  9668  qreccl  9671  xleaddadd  9916  ixxss12  9935  ioodisj  10022  fznlem  10070  elfz0fzfz0  10155  btwnzge0  10330  mulexpzap  10590  leexp1a  10605  expnbnd  10674  hashennnuni  10790  zfz1iso  10852  seq3coll  10853  resqrexlemga  11063  sqrtsq  11084  abs3lem  11151  cau3lem  11154  minmax  11269  xrmaxiflemval  11289  xrminmax  11304  climcau  11386  summodclem2  11421  fsumrelem  11510  cvgratz  11571  mertenslemi1  11574  mertenslem2  11575  mertensabs  11576  fprodcl2lem  11644  fprodap0  11660  fprodrec  11668  fprodap0f  11675  fprodle  11679  dvdsle  11881  bezoutlemmain  12030  bezoutlemzz  12034  dfgcd3  12042  dvdsmulgcd  12057  lcmcllem  12098  lcmgcdlem  12108  ncoprmgcdne1b  12120  qredeu  12128  oddpwdclemxy  12200  oddpwdclemdc  12204  pythagtriplem2  12297  pythagtrip  12314  pc2dvds  12361  pcz  12363  ctiunctlemfo  12489  unct  12492  sgrppropd  12873  mndpropd  12898  mhmeql  12941  mhmid  13054  mhmmnd  13055  mulgval  13061  issubg4m  13129  imasabl  13270  reldvdsrsrg  13439  dvdsrmul1  13449  unitgrp  13463  neissex  14117  restbasg  14120  tgrest  14121  restopnb  14133  cnptopco  14174  metequiv2  14448  xmettx  14462  metcnpi3  14469  fsumcncntop  14508  elcncf2  14513  cncfmet  14531  dedekindeulemuub  14547  dedekindeulemlu  14551  dedekindicclemuub  14556  dedekindicclemlu  14560  limccnpcntop  14596  reeff1olem  14644  nninfalllem1  15211  apdiff  15250