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

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

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 969 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
21adantr 272 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  frirrg  4232  fidceq  6716  fidifsnen  6717  en2eqpr  6754  iunfidisj  6786  ordiso2  6872  addlocpr  7289  aptiprlemu  7393  xltadd1  9549  xlesubadd  9556  icoshftf1o  9664  fztri3or  9709  elfzonelfzo  9897  exp3val  10185  hashun  10441  subcn2  10969  divalglemeuneg  11465  dvdslegcd  11498  lcmledvds  11594  rpdvds  11623  cncongr2  11628  iuncld  12124  iscnp4  12226  cnpnei  12227  cnconst2  12241  cnpdis  12250  txcn  12283  blssps  12413  blss  12414  metcnp3  12497  metcnp  12498
  Copyright terms: Public domain W3C validator