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

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

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 971 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
21adantr 274 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947
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 949
This theorem is referenced by:  frirrg  4242  fidceq  6731  fidifsnen  6732  en2eqpr  6769  iunfidisj  6802  ordiso2  6888  addlocpr  7312  aptiprlemu  7416  xltadd1  9627  xlesubadd  9634  icoshftf1o  9742  fztri3or  9787  elfzonelfzo  9975  exp3val  10263  hashun  10519  subcn2  11048  divalglemeuneg  11547  dvdslegcd  11580  lcmledvds  11678  rpdvds  11707  cncongr2  11712  iuncld  12211  iscnp4  12314  cnpnei  12315  cnconst2  12329  cnpdis  12338  txcn  12371  blssps  12523  blss  12524  metcnp3  12607  metcnp  12608
  Copyright terms: Public domain W3C validator