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

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

Proof of Theorem simp1l3
StepHypRef Expression
1 simpl3 1239 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
213ad2ant1 1156 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  btwnconn1lem7  32519  btwnconn1lem12  32524  linethru  32579  hlrelat3  35190  cvrval3  35191  2atlt  35217  atbtwnex  35226  1cvratlt  35252  2llnmat  35302  lplnexllnN  35342  4atlem11  35387  lnjatN  35558  lncvrat  35560  lncmp  35561  cdlemd9  35985  dihord5b  37038  dihmeetALTN  37106  dih1dimatlem0  37107  mapdrvallem2  37424
  Copyright terms: Public domain W3C validator