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

Theorem simpll1 1038
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 1002 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantr 276 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
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  6899  ordiso2  7065  ctssdc  7143  addlocpr  7566  xltadd1  9908  nn0ltexp2  10724  hashun  10820  fimaxq  10842  xrmaxltsup  11301  dvdslegcd  12000  lcmledvds  12105  divgcdcoprm0  12136  rpexp  12188  qexpz  12387  dfgrp3mlem  13057  rhmdvdsr  13542  rnglidlmcl  13813  iscnp4  14195  cnconst2  14210  blssps  14404  blss  14405  metcnp  14489  addcncntoplem  14528  cdivcncfap  14564  lgsfvalg  14884  lgsmod  14905  lgsdir  14914  lgsne0  14917
  Copyright terms: Public domain W3C validator