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

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

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 996 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantr 274 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 974
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 976
This theorem is referenced by:  fidifsnen  6852  ordiso2  7016  ctssdc  7094  addlocpr  7502  xltadd1  9837  nn0ltexp2  10648  hashun  10744  fimaxq  10766  xrmaxltsup  11225  dvdslegcd  11923  lcmledvds  12028  divgcdcoprm0  12059  rpexp  12111  qexpz  12308  dfgrp3mlem  12801  iscnp4  13097  cnconst2  13112  blssps  13306  blss  13307  metcnp  13391  addcncntoplem  13430  cdivcncfap  13466  lgsfvalg  13785  lgsmod  13806  lgsdir  13815  lgsne0  13818
  Copyright terms: Public domain W3C validator