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

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

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 1242 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
213ad2ant1 1163 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 1109
This theorem is referenced by:  mapxpen  8332  lsmcv  19413  archiabl  30133  trisegint  32510  linethru  32635  hlrelat3  35300  cvrval3  35301  cvrval4N  35302  2atlt  35327  atbtwnex  35336  1cvratlt  35362  atcvrlln2  35407  atcvrlln  35408  2llnmat  35412  lplnexllnN  35452  lvolnlelpln  35473  lnjatN  35668  lncvrat  35670  lncmp  35671  cdlemd9  36094  dihord5b  37147  dihmeetALTN  37215  dih1dimatlem0  37216  mapdrvallem2  37533
  Copyright terms: Public domain W3C validator