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

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

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 995 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantr 274 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 973
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 975
This theorem is referenced by:  fidifsnen  6846  ordiso2  7010  ctssdc  7088  addlocpr  7491  xltadd1  9826  nn0ltexp2  10637  hashun  10733  fimaxq  10755  xrmaxltsup  11214  dvdslegcd  11912  lcmledvds  12017  divgcdcoprm0  12048  rpexp  12100  qexpz  12297  iscnp4  12977  cnconst2  12992  blssps  13186  blss  13187  metcnp  13271  addcncntoplem  13310  cdivcncfap  13346  lgsfvalg  13665  lgsmod  13686  lgsdir  13695  lgsne0  13698
  Copyright terms: Public domain W3C validator