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

Theorem simpll3 1040
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 1004 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 276 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  frirrg  4396  fidceq  6965  fidifsnen  6966  en2eqpr  7003  iunfidisj  7047  ordiso2  7136  addlocpr  7648  aptiprlemu  7752  xltadd1  9997  xlesubadd  10004  icoshftf1o  10112  fztri3or  10160  elfzonelfzo  10357  exp3val  10684  nn0ltexp2  10852  hashun  10948  subcn2  11593  divalglemeuneg  12205  dvdslegcd  12256  lcmledvds  12363  rpdvds  12392  cncongr2  12397  qexpz  12646  iuncld  14558  iscnp4  14661  cnpnei  14662  cnconst2  14676  cnpdis  14685  txcn  14718  blssps  14870  blss  14871  metcnp3  14954  metcnp  14955  lgsfcl2  15454  lgsdir  15483  lgsne0  15486
  Copyright terms: Public domain W3C validator