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

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

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1191 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
213ad2ant1 1132 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 206  df-an 396  df-3an 1088
This theorem is referenced by:  poxp3  8141  mapxpen  9149  lsmcv  20988  pmatcollpw2  22601  sltlpss  27748  btwnconn1lem4  35534  linethru  35597  hlrelat3  38750  cvrval3  38751  cvrval4N  38752  2atlt  38777  atbtwnex  38786  1cvratlt  38812  atcvrlln2  38857  atcvrlln  38858  2llnmat  38862  lvolnlelpln  38923  lnjatN  39118  lncmp  39121  cdlemd9  39544  dihord5b  40597  dihmeetALTN  40665  mapdrvallem2  40983  itschlc0xyqsol  47618
  Copyright terms: Public domain W3C validator