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

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

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1065 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
213ad2ant1 1082 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037
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 1039
This theorem is referenced by:  mapxpen  8126  lsmcv  19141  pmatcollpw2  20583  btwnconn1lem4  32197  linethru  32260  hlrelat3  34698  cvrval3  34699  cvrval4N  34700  2atlt  34725  atbtwnex  34734  1cvratlt  34760  atcvrlln2  34805  atcvrlln  34806  2llnmat  34810  lvolnlelpln  34871  lnjatN  35066  lncmp  35069  cdlemd9  35493  dihord5b  36548  dihmeetALTN  36616  mapdrvallem2  36934
  Copyright terms: Public domain W3C validator