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

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

Proof of Theorem simp1l3
StepHypRef Expression
1 simpl3 1064 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
213ad2ant1 1080 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  btwnconn1lem7  31842  btwnconn1lem12  31847  linethru  31902  hlrelat3  34178  cvrval3  34179  2atlt  34205  atbtwnex  34214  1cvratlt  34240  2llnmat  34290  lplnexllnN  34330  4atlem11  34375  lnjatN  34546  lncvrat  34548  lncmp  34549  cdlemd9  34973  dihord5b  36028  dihmeetALTN  36096  dih1dimatlem0  36097  mapdrvallem2  36414
  Copyright terms: Public domain W3C validator