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

Theorem simpll3 1023
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 987 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 274 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963
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 965
This theorem is referenced by:  frirrg  4310  fidceq  6814  fidifsnen  6815  en2eqpr  6852  iunfidisj  6890  ordiso2  6979  addlocpr  7456  aptiprlemu  7560  xltadd1  9780  xlesubadd  9787  icoshftf1o  9895  fztri3or  9941  elfzonelfzo  10129  exp3val  10421  hashun  10679  subcn2  11208  divalglemeuneg  11814  dvdslegcd  11848  lcmledvds  11947  rpdvds  11976  cncongr2  11981  iuncld  12526  iscnp4  12629  cnpnei  12630  cnconst2  12644  cnpdis  12653  txcn  12686  blssps  12838  blss  12839  metcnp3  12922  metcnp  12923
  Copyright terms: Public domain W3C validator