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

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

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 986 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
21adantr 274 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
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 965
This theorem is referenced by:  fidceq  6816  fidifsnen  6817  en2eqpr  6854  iunfidisj  6892  ctssdc  7059  cauappcvgprlemlol  7569  caucvgprlemlol  7592  caucvgprprlemlol  7620  elfzonelfzo  10138  qbtwnre  10165  nn0ltexp2  10595  hashun  10690  xrmaxltsup  11166  subcn2  11219  prodmodclem2  11485  divalglemex  11825  divalglemeuneg  11826  dvdslegcd  11863  lcmledvds  11962  modprmn0modprm0  12146  iscnp4  12688  cnrest2  12706  blssps  12897  blss  12898  bdbl  12973  metcnp3  12981  addcncntoplem  13021  cdivcncfap  13057
  Copyright terms: Public domain W3C validator