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

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

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 969 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantr 274 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )
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
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  fidifsnen  6732  ordiso2  6888  ctssdc  6966  addlocpr  7312  xltadd1  9627  hashun  10519  fimaxq  10541  xrmaxltsup  10995  dvdslegcd  11580  lcmledvds  11678  divgcdcoprm0  11709  rpexp  11758  iscnp4  12314  cnconst2  12329  blssps  12523  blss  12524  metcnp  12608  addcncntoplem  12647  cdivcncfap  12683
  Copyright terms: Public domain W3C validator