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

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

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1237 . 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:  mapxpen  8374  lsmcv  19368  pmatcollpw2  20816  btwnconn1lem4  32539  linethru  32602  hlrelat3  35210  cvrval3  35211  cvrval4N  35212  2atlt  35237  atbtwnex  35246  1cvratlt  35272  atcvrlln2  35317  atcvrlln  35318  2llnmat  35322  lvolnlelpln  35383  lnjatN  35578  lncmp  35581  cdlemd9  36004  dihord5b  37057  dihmeetALTN  37125  mapdrvallem2  37443
  Copyright terms: Public domain W3C validator