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

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

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 1188 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
213ad2ant1 1130 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084
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 395  df-3an 1086
This theorem is referenced by:  poxp3  8155  mapxpen  9168  lsmcv  21041  sltlpss  27879  archiabl  32998  trisegint  35755  linethru  35880  hlrelat3  39015  cvrval3  39016  cvrval4N  39017  2atlt  39042  atbtwnex  39051  1cvratlt  39077  atcvrlln2  39122  atcvrlln  39123  2llnmat  39127  lplnexllnN  39167  lvolnlelpln  39188  lnjatN  39383  lncvrat  39385  lncmp  39386  cdlemd9  39809  dihord5b  40862  dihmeetALTN  40930  dih1dimatlem0  40931  mapdrvallem2  41248  grumnudlem  43864
  Copyright terms: Public domain W3C validator