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  5983  suppcofn  6510  tfrlem1  6584  phplem4dom  7169  phplem4on  7175  fisseneq  7248  suplub2ti  7347  omp1eomlem  7440  nnnninfeq  7474  nninfisol  7479  exmidontriim  7587  addcmpblnq  7740  mulcmpblnq  7741  ordpipqqs  7747  ltexnqq  7781  enq0tr  7807  addcmpblnq0  7816  mulcmpblnq0  7817  nnnq0lem1  7819  prssnql  7852  prmuloc  7939  prmuloc2  7940  mullocpr  7944  ltexprlemopu  7976  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  ltmprr  8015  archpr  8016  suplocexprlemloc  8094  addcmpblnr  8112  mulcmpblnrlemg  8113  mulcmpblnr  8114  ltsrprg  8120  srpospr  8156  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  negeu  8524  add20  8809  rimul  8921  apreap  8923  cru  8938  mulge0  8955  mulap0  8990  prodgt0  9190  ltmul12a  9198  ledivdiv  9228  lediv12a  9232  qapne  10054  qreccl  10057  irraddap  10062  xleaddadd  10305  ixxss12  10324  ioodisj  10411  fznlem  10461  elfz0fzfz0  10549  btwnzge0  10755  seqf1og  10978  mulexpzap  11036  leexp1a  11051  expnbnd  11121  hashennnuni  11239  hashf1lem2  11307  zfz1iso  11314  seq3coll  11315  swrdswrdlem  11497  pfxccatin12lem3  11525  resqrexlemga  11810  sqrtsq  11831  abs3lem  11899  cau3lem  11902  minmax  12019  xrmaxiflemval  12040  xrminmax  12055  climcau  12137  summodclem2  12173  fsumrelem  12262  cvgratz  12323  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  fprodcl2lem  12396  fprodap0  12412  fprodrec  12420  fprodap0f  12427  fprodle  12431  dvdsle  12635  bitsfzo  12746  bezoutlemmain  12799  bezoutlemzz  12803  dfgcd3  12811  dvdsmulgcd  12826  lcmcllem  12869  lcmgcdlem  12879  ncoprmgcdne1b  12891  qredeu  12899  pwbdvdseu  12971  nnmaxpwlemparts  12976  pythagtriplem2  13073  pythagtrip  13090  pc2dvds  13137  pcz  13139  ctiunctlemfo  13387  unct  13390  sgrppropd  13786  mndpropd  13811  mhmeql  13857  mhmid  13976  mhmmnd  13977  mulgval  13983  issubg4m  14054  imasabl  14229  gzsumconst  14232  gsumzfi  14247  gsummptfidmadd  14250  gsummptfidmsplit  14253  dvdsrmul1  14517  unitgrp  14531  aprlring  14708  gsumfsum  15031  issubassa2  15143  neissex  15408  restbasg  15411  tgrest  15412  restopnb  15424  cnptopco  15465  metequiv2  15739  xmettx  15753  metcnpi3  15760  mpomulcn  15809  fsumcncntop  15810  elcncf2  15817  cncfmet  15835  dedekindeulemuub  15860  dedekindeulemlu  15864  dedekindicclemuub  15869  dedekindicclemlu  15873  limccnpcntop  15918  dvmptfsum  15968  reeff1olem  16014  lgsquad3  16425  clwwlkccatlem  16863  nninfalllem1  17274  nninfnfiinf  17289  apdiff  17321