ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simplll Unicode version

Theorem simplll 493
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
StepHypRef Expression
1 simpl 106 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 465 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  f1imass  5440  tfrlem1  5953  phplem4dom  6354  phplem4on  6359  addcmpblnq  6522  mulcmpblnq  6523  ordpipqqs  6529  ltexnqq  6563  enq0tr  6589  addcmpblnq0  6598  mulcmpblnq0  6599  nnnq0lem1  6601  prssnql  6634  prmuloc  6721  prmuloc2  6722  mullocpr  6726  ltexprlemopu  6758  ltexprlemrl  6765  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  ltmprr  6797  archpr  6798  addcmpblnr  6881  mulcmpblnrlemg  6882  mulcmpblnr  6883  ltsrprg  6889  srpospr  6924  axcaucvglemres  7030  negeu  7264  add20  7542  rimul  7649  apreap  7651  cru  7666  mulge0  7683  mulap0  7708  prodgt0  7892  ltmul12a  7900  ledivdiv  7930  lediv12a  7934  qapne  8670  qreccl  8673  ixxss12  8875  ioodisj  8961  fznlem  9006  elfz0fzfz0  9084  btwnzge0  9249  mulexpzap  9459  leexp1a  9474  expnbnd  9539  resqrexlemga  9849  sqrtsq  9870  abs3lem  9937  cau3lem  9940  climcau  10096  dvdsle  10155  oddpwdclemxy  10236  oddpwdclemdc  10240
  Copyright terms: Public domain W3C validator