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

Theorem simp3r 995
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 989 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 947
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 949
This theorem is referenced by:  simpl3r  1022  simpr3r  1028  simp13r  1082  simp23r  1088  simp33r  1094  issod  4211  tfisi  4471  fvun1  5455  f1oiso2  5696  tfrlem5  6179  tfr1onlembxssdm  6208  tfrcllembxssdm  6221  ecopovtrn  6494  ecopovtrng  6497  addassnqg  7158  ltsonq  7174  ltanqg  7176  ltmnqg  7177  addassnq0  7238  mulasssrg  7534  distrsrg  7535  lttrsr  7538  ltsosr  7540  ltasrg  7546  mulextsr1lem  7556  mulextsr1  7557  axmulass  7649  axdistr  7650  reapmul1  8325  mulcanap  8394  mulcanap2  8395  divassap  8418  divdirap  8425  div11ap  8428  apmul1  8516  ltdiv1  8594  ltmuldiv  8600  ledivmul  8603  lemuldiv  8607  lediv2  8617  ltdiv23  8618  lediv23  8619  xaddass2  9621  xlt2add  9631  modqdi  10133  expaddzap  10305  expmulzap  10307  leisorel  10548  resqrtcl  10769  xrbdtri  11013  dvdsgcd  11627  rpexp12i  11760  psmetlecl  12430  xmetlecl  12463  xblcntrps  12509  xblcntr  12510
  Copyright terms: Public domain W3C validator