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

Theorem simpll3 1038
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 1002 . 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 978
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 980
This theorem is referenced by:  frirrg  4350  fidceq  6868  fidifsnen  6869  en2eqpr  6906  iunfidisj  6944  ordiso2  7033  addlocpr  7534  aptiprlemu  7638  xltadd1  9874  xlesubadd  9881  icoshftf1o  9989  fztri3or  10036  elfzonelfzo  10227  exp3val  10519  nn0ltexp2  10685  hashun  10780  subcn2  11314  divalglemeuneg  11922  dvdslegcd  11959  lcmledvds  12064  rpdvds  12093  cncongr2  12098  qexpz  12344  iuncld  13508  iscnp4  13611  cnpnei  13612  cnconst2  13626  cnpdis  13635  txcn  13668  blssps  13820  blss  13821  metcnp3  13904  metcnp  13905  lgsfcl2  14300  lgsdir  14329  lgsne0  14332
  Copyright terms: Public domain W3C validator