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

Theorem simplrl 495
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplrl  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ps )

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 106 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antlr 466 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ps )
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:  rmob  2878  f1imass  5441  riota5f  5520  tfrexlem  5979  fopwdom  6341  fidceq  6361  fisbth  6371  fientri3  6384  ordiso2  6415  addcmpblnq  6523  mulcmpblnq  6524  ordpipqqs  6530  addcmpblnq0  6599  mulcmpblnq0  6600  prml  6633  addlocpr  6692  prmuloc  6722  mullocpr  6727  ltexprlemopl  6757  ltexprlemopu  6759  ltexprlemloc  6763  ltexprlemrl  6766  ltexprlemru  6768  addcanprleml  6770  addcanprlemu  6771  aptiprleml  6795  ltmprr  6798  cauappcvgprlemopl  6802  cauappcvgprlemopu  6804  cauappcvgprlemloc  6808  caucvgprlemopl  6825  caucvgprlemopu  6827  caucvgprlemloc  6831  caucvgprprlemopu  6855  caucvgprprlemloc  6859  caucvgprprlemexbt  6862  caucvgprprlemaddq  6864  addcmpblnr  6882  mulcmpblnrlemg  6883  mulcmpblnr  6884  ltsrprg  6890  mulgt0sr  6920  caucvgsrlemgt1  6937  axmulcl  7000  axcaucvglemres  7031  cnegexlem1  7249  negeu  7265  add20  7543  apreap  7652  cru  7667  apsym  7671  apcotr  7672  apadd1  7673  apneg  7676  mulext1  7677  mulge0  7684  mulap0  7709  divdivdivap  7764  prodgt0  7893  ltmul12a  7901  lt2mul2div  7920  ledivdiv  7931  lediv12a  7935  qapne  8671  ixxss12  8876  elfz0ubfz0  9084  qtri3or  9200  qbtwnzlemstep  9205  qbtwnzlemex  9207  qbtwnz  9208  rebtwn2zlemstep  9209  rebtwn2z  9211  btwnzge0  9250  expivallem  9421  mulexpzap  9460  leexp1a  9475  cjap  9734  cvg1nlemres  9812  rsqrmo  9854  abslt  9915  abs3lem  9938  cau3lem  9941  climcau  10097  divalglemeunn  10233  divalglemeuneg  10235  pw2dvdseu  10256  qdencn  10511
  Copyright terms: Public domain W3C validator