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

Theorem simpll3 1005
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll3  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 969 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 272 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
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:  frirrg  4240  fidceq  6729  fidifsnen  6730  en2eqpr  6767  iunfidisj  6800  ordiso2  6886  addlocpr  7308  aptiprlemu  7412  xltadd1  9610  xlesubadd  9617  icoshftf1o  9725  fztri3or  9770  elfzonelfzo  9958  exp3val  10246  hashun  10502  subcn2  11031  divalglemeuneg  11527  dvdslegcd  11560  lcmledvds  11658  rpdvds  11687  cncongr2  11692  iuncld  12190  iscnp4  12293  cnpnei  12294  cnconst2  12308  cnpdis  12317  txcn  12350  blssps  12502  blss  12503  metcnp3  12586  metcnp  12587
  Copyright terms: Public domain W3C validator