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

Theorem simp3r 993
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 109 . 2  |-  ( ( ch  /\  th )  ->  th )
213ad2ant3 987 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  simpl3r  1020  simpr3r  1026  simp13r  1080  simp23r  1086  simp33r  1092  issod  4209  tfisi  4469  fvun1  5453  f1oiso2  5694  tfrlem5  6177  tfr1onlembxssdm  6206  tfrcllembxssdm  6219  ecopovtrn  6492  ecopovtrng  6495  addassnqg  7154  ltsonq  7170  ltanqg  7172  ltmnqg  7173  addassnq0  7234  mulasssrg  7530  distrsrg  7531  lttrsr  7534  ltsosr  7536  ltasrg  7542  mulextsr1lem  7552  mulextsr1  7553  axmulass  7645  axdistr  7646  reapmul1  8320  mulcanap  8389  mulcanap2  8390  divassap  8413  divdirap  8420  div11ap  8423  apmul1  8511  ltdiv1  8586  ltmuldiv  8592  ledivmul  8595  lemuldiv  8599  lediv2  8609  ltdiv23  8610  lediv23  8611  xaddass2  9604  xlt2add  9614  modqdi  10116  expaddzap  10288  expmulzap  10290  leisorel  10531  resqrtcl  10752  xrbdtri  10996  dvdsgcd  11607  rpexp12i  11740  psmetlecl  12409  xmetlecl  12442  xblcntrps  12488  xblcntr  12489
  Copyright terms: Public domain W3C validator