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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 108 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 989 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
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:  simpl3l  1021  simpr3l  1027  simp13l  1081  simp23l  1087  simp33l  1093  issod  4211  tfisi  4471  tfrlem5  6179  tfrlemibxssdm  6192  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  lemul1  8323  reapmul1lem  8324  reapmul1  8325  mulcanap  8394  mulcanap2  8395  divassap  8418  divdirap  8425  div11ap  8428  muldivdirap  8435  divcanap5  8442  apmul1  8516  apmul2  8517  ltdiv1  8594  ltmuldiv  8600  ledivmul  8603  lemuldiv  8607  ltdiv2  8613  lediv2  8617  ltdiv23  8618  lediv23  8619  xaddass2  9621  xlt2add  9631  modqdi  10133  expaddzap  10305  expmulzap  10307  leisorel  10548  resqrtcl  10769  xrbdtri  11013  dvdscmulr  11449  dvdsmulcr  11450  dvdsadd2b  11467  dvdsgcd  11627  rpexp12i  11760  psmetlecl  12430  xmetlecl  12463
  Copyright terms: Public domain W3C validator