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

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

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 987 . 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  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 965 This theorem is referenced by:  frirrg  4281  fidceq  6772  fidifsnen  6773  en2eqpr  6810  iunfidisj  6844  ordiso2  6930  addlocpr  7388  aptiprlemu  7492  xltadd1  9709  xlesubadd  9716  icoshftf1o  9824  fztri3or  9870  elfzonelfzo  10058  exp3val  10346  hashun  10603  subcn2  11132  divalglemeuneg  11676  dvdslegcd  11709  lcmledvds  11807  rpdvds  11836  cncongr2  11841  iuncld  12343  iscnp4  12446  cnpnei  12447  cnconst2  12461  cnpdis  12470  txcn  12503  blssps  12655  blss  12656  metcnp3  12739  metcnp  12740
 Copyright terms: Public domain W3C validator