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

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

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 948 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
21adantr 271 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 925
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 927
This theorem is referenced by:  fidceq  6639  fidifsnen  6640  en2eqpr  6677  iunfidisj  6709  cauappcvgprlemlol  7267  caucvgprlemlol  7290  caucvgprprlemlol  7318  elfzonelfzo  9702  qbtwnre  9729  hashun  10274  subcn2  10761  divalglemex  11261  divalglemeuneg  11262  dvdslegcd  11295  lcmledvds  11391
  Copyright terms: Public domain W3C validator