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

Theorem simpll1 1038
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 1002 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantr 276 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )
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
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  fidifsnen  6898  ordiso2  7064  ctssdc  7142  addlocpr  7565  xltadd1  9906  nn0ltexp2  10721  hashun  10817  fimaxq  10839  xrmaxltsup  11298  dvdslegcd  11997  lcmledvds  12102  divgcdcoprm0  12133  rpexp  12185  qexpz  12384  dfgrp3mlem  13042  rhmdvdsr  13525  rnglidlmcl  13796  iscnp4  14175  cnconst2  14190  blssps  14384  blss  14385  metcnp  14469  addcncntoplem  14508  cdivcncfap  14544  lgsfvalg  14864  lgsmod  14885  lgsdir  14894  lgsne0  14897
  Copyright terms: Public domain W3C validator