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

Theorem simp3r 944
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3r  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 107 . 2  |-  ( ( ch  /\  th )  ->  th )
213ad2ant3 938 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
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 depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpl3r  971  simpr3r  977  simp13r  1031  simp23r  1037  simp33r  1043  issod  4084  tfisi  4338  fvun1  5267  f1oiso2  5494  tfrlem5  5961  ecopovtrn  6234  ecopovtrng  6237  addassnqg  6538  ltsonq  6554  ltanqg  6556  ltmnqg  6557  addassnq0  6618  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltsosr  6907  ltasrg  6913  mulextsr1lem  6922  mulextsr1  6923  axmulass  7005  axdistr  7006  reapmul1  7660  mulcanap  7720  mulcanap2  7721  divassap  7743  divdirap  7748  div11ap  7751  apmul1  7839  ltdiv1  7909  ltmuldiv  7915  ledivmul  7918  lemuldiv  7922  lediv2  7932  ltdiv23  7933  lediv23  7934  modqdi  9342  expaddzap  9464  expmulzap  9466  resqrtcl  9856
  Copyright terms: Public domain W3C validator