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

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

Proof of Theorem simp1l3
StepHypRef Expression
1 simpl3 1231 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
213ad2ant1 1127 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  btwnconn1lem7  32530  btwnconn1lem12  32535  linethru  32590  hlrelat3  35213  cvrval3  35214  2atlt  35240  atbtwnex  35249  1cvratlt  35275  2llnmat  35325  lplnexllnN  35365  4atlem11  35410  lnjatN  35581  lncvrat  35583  lncmp  35584  cdlemd9  36008  dihord5b  37062  dihmeetALTN  37130  dih1dimatlem0  37131  mapdrvallem2  37448
  Copyright terms: Public domain W3C validator