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

Theorem simp3r 970
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 108 . 2  |-  ( ( ch  /\  th )  ->  th )
213ad2ant3 964 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  simpl3r  997  simpr3r  1003  simp13r  1057  simp23r  1063  simp33r  1069  issod  4122  tfisi  4377  fvun1  5335  f1oiso2  5569  tfrlem5  6035  tfr1onlembxssdm  6064  tfrcllembxssdm  6077  ecopovtrn  6343  ecopovtrng  6346  addassnqg  6888  ltsonq  6904  ltanqg  6906  ltmnqg  6907  addassnq0  6968  mulasssrg  7251  distrsrg  7252  lttrsr  7255  ltsosr  7257  ltasrg  7263  mulextsr1lem  7272  mulextsr1  7273  axmulass  7355  axdistr  7356  reapmul1  8016  mulcanap  8076  mulcanap2  8077  divassap  8099  divdirap  8106  div11ap  8109  apmul1  8197  ltdiv1  8267  ltmuldiv  8273  ledivmul  8276  lemuldiv  8280  lediv2  8290  ltdiv23  8291  lediv23  8292  modqdi  9730  expaddzap  9901  expmulzap  9903  leisorel  10142  resqrtcl  10361  dvdsgcd  10907  rpexp12i  11040
  Copyright terms: Public domain W3C validator