Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1l3 Structured version   Visualization version   GIF version

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

Proof of Theorem simp1l3
StepHypRef Expression
1 simpl3 1059 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
213ad2ant1 1075 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033 This theorem is referenced by:  btwnconn1lem7  31370  btwnconn1lem12  31375  linethru  31430  hlrelat3  33716  cvrval3  33717  2atlt  33743  atbtwnex  33752  1cvratlt  33778  2llnmat  33828  lplnexllnN  33868  4atlem11  33913  lnjatN  34084  lncvrat  34086  lncmp  34087  cdlemd9  34511  dihord5b  35566  dihmeetALTN  35634  dih1dimatlem0  35635  mapdrvallem2  35952
 Copyright terms: Public domain W3C validator