MPE Home 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