Theorem simplll 535

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  543  f1imass  5925  suppcofn  6444  tfrlem1  6517  phplem4dom  7091  phplem4on  7097  fisseneq  7170  suplub2ti  7243  omp1eomlem  7336  nnnninfeq  7370  nninfisol  7375  exmidontriim  7483  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  ltexnqq  7671  enq0tr  7697  addcmpblnq0  7706  mulcmpblnq0  7707  nnnq0lem1  7709  prssnql  7742  prmuloc  7829  prmuloc2  7830  mullocpr  7834  ltexprlemopu  7866  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  ltmprr  7905  archpr  7906  suplocexprlemloc  7984  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  ltsrprg  8010  srpospr  8046  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  negeu  8412  add20  8696  rimul  8807  apreap  8809  cru  8824  mulge0  8841  mulap0  8876  prodgt0  9074  ltmul12a  9082  ledivdiv  9112  lediv12a  9116  qapne  9917  qreccl  9920  xleaddadd  10166  ixxss12  10185  ioodisj  10272  fznlem  10321  elfz0fzfz0  10406  btwnzge0  10606  seqf1og  10829  mulexpzap  10887  leexp1a  10902  expnbnd  10971  hashennnuni  11087  zfz1iso  11151  seq3coll  11152  swrdswrdlem  11334  pfxccatin12lem3  11362  resqrexlemga  11646  sqrtsq  11667  abs3lem  11734  cau3lem  11737  minmax  11853  xrmaxiflemval  11873  xrminmax  11888  climcau  11970  summodclem2  12006  fsumrelem  12095  cvgratz  12156  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  fprodcl2lem  12229  fprodap0  12245  fprodrec  12253  fprodap0f  12260  fprodle  12264  dvdsle  12468  bitsfzo  12579  bezoutlemmain  12632  bezoutlemzz  12636  dfgcd3  12644  dvdsmulgcd  12659  lcmcllem  12702  lcmgcdlem  12712  ncoprmgcdne1b  12724  qredeu  12732  oddpwdclemxy  12804  oddpwdclemdc  12808  pythagtriplem2  12902  pythagtrip  12919  pc2dvds  12966  pcz  12968  ctiunctlemfo  13123  unct  13126  sgrppropd  13559  mndpropd  13586  mhmeql  13638  mhmid  13765  mhmmnd  13766  mulgval  13772  issubg4m  13843  imasabl  13986  gsumfzconst  13991  dvdsrmul1  14180  unitgrp  14194  neissex  14959  restbasg  14962  tgrest  14963  restopnb  14975  cnptopco  15016  metequiv2  15290  xmettx  15304  metcnpi3  15311  mpomulcn  15360  fsumcncntop  15361  elcncf2  15368  cncfmet  15386  dedekindeulemuub  15411  dedekindeulemlu  15415  dedekindicclemuub  15420  dedekindicclemlu  15424  limccnpcntop  15469  dvmptfsum  15519  reeff1olem  15565  lgsquad3  15886  clwwlkccatlem  16324  nninfalllem1  16717  nninfnfiinf  16732  apdiff  16763