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

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

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 952 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantr 272 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  fidifsnen  6693  ordiso2  6835  ctssdc  6912  addlocpr  7245  xltadd1  9500  hashun  10392  fimaxq  10414  xrmaxltsup  10866  dvdslegcd  11448  lcmledvds  11544  divgcdcoprm0  11575  rpexp  11624  iscnp4  12168  cnconst2  12183  blssps  12355  blss  12356  metcnp  12436  cdivcncfap  12499
  Copyright terms: Public domain W3C validator