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

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

Proof of Theorem simp1l3
StepHypRef Expression
1 simpl3 1191 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
213ad2ant1 1131 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085
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 1087
This theorem is referenced by:  poxp3  8149  btwnconn1lem7  35683  btwnconn1lem12  35688  linethru  35743  hlrelat3  38879  cvrval3  38880  2atlt  38906  atbtwnex  38915  1cvratlt  38941  2llnmat  38991  lplnexllnN  39031  4atlem11  39076  lnjatN  39247  lncvrat  39249  lncmp  39250  cdlemd9  39673  dihord5b  40726  dihmeetALTN  40794  dih1dimatlem0  40795  mapdrvallem2  41112  grumnudlem  43716  itsclc0yqsol  47831  itschlc0xyqsol  47834
  Copyright terms: Public domain W3C validator