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

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

Proof of Theorem simp1l3
StepHypRef Expression
1 simpl3 1190 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
213ad2ant1 1130 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  btwnconn1lem7  33668  btwnconn1lem12  33673  linethru  33728  hlrelat3  36707  cvrval3  36708  2atlt  36734  atbtwnex  36743  1cvratlt  36769  2llnmat  36819  lplnexllnN  36859  4atlem11  36904  lnjatN  37075  lncvrat  37077  lncmp  37078  cdlemd9  37501  dihord5b  38554  dihmeetALTN  38622  dih1dimatlem0  38623  mapdrvallem2  38940  grumnudlem  40990  itsclc0yqsol  45175  itschlc0xyqsol  45178
 Copyright terms: Public domain W3C validator