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

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

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 984 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantr 274 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 962
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 964
This theorem is referenced by:  fidifsnen  6764  ordiso2  6920  ctssdc  6998  addlocpr  7356  xltadd1  9671  hashun  10563  fimaxq  10585  xrmaxltsup  11039  dvdslegcd  11664  lcmledvds  11762  divgcdcoprm0  11793  rpexp  11842  iscnp4  12401  cnconst2  12416  blssps  12610  blss  12611  metcnp  12695  addcncntoplem  12734  cdivcncfap  12770
  Copyright terms: Public domain W3C validator