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

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

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 1004 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
21adantr 276 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  frirrg  4368  fidceq  6896  fidifsnen  6897  en2eqpr  6934  iunfidisj  6974  ordiso2  7063  addlocpr  7564  aptiprlemu  7668  xltadd1  9905  xlesubadd  9912  icoshftf1o  10020  fztri3or  10068  elfzonelfzo  10259  exp3val  10552  nn0ltexp2  10720  hashun  10816  subcn2  11350  divalglemeuneg  11959  dvdslegcd  11996  lcmledvds  12101  rpdvds  12130  cncongr2  12135  qexpz  12383  iuncld  14067  iscnp4  14170  cnpnei  14171  cnconst2  14185  cnpdis  14194  txcn  14227  blssps  14379  blss  14380  metcnp3  14463  metcnp  14464  lgsfcl2  14860  lgsdir  14889  lgsne0  14892
  Copyright terms: Public domain W3C validator