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

Theorem simpl11 1322
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpl11 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜑)

Proof of Theorem simpl11
StepHypRef Expression
1 simpl1 1235 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜑)
213ad2antl1 1229 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 1102
This theorem is referenced by:  pythagtriplem4  15744  tsmsxp  22175  brbtwn2  26005  ax5seg  26038  3vfriswmgr  27459  br8  31973  nolt02o  32171  btwndiff  32460  ifscgr  32477  seglecgr12im  32543  lkrshp  34887  cvlcvr1  35121  atbtwn  35228  3dimlem3  35243  3dimlem3OLDN  35244  1cvratex  35255  llnmlplnN  35321  4atlem3  35378  4atlem3a  35379  4atlem11  35391  4atlem12  35394  lnatexN  35561  cdlemb  35576  paddasslem4  35605  paddasslem10  35611  pmodlem1  35628  llnexchb2lem  35650  llnexchb2  35651  arglem1N  35972  cdlemd4  35983  cdlemd9  35988  cdlemd  35989  cdleme16  36067  cdleme20  36106  cdleme21i  36117  cdleme21k  36120  cdleme27N  36151  cdleme28c  36154  cdlemefrs29bpre0  36178  cdlemefrs29clN  36181  cdlemefrs32fva  36182  cdleme41sn3a  36215  cdleme32fva  36219  cdleme40n  36250  cdlemg12e  36429  cdlemg15a  36437  cdlemg15  36438  cdlemg16ALTN  36440  cdlemg16z  36441  cdlemg20  36467  cdlemg22  36469  cdlemg29  36487  cdlemg38  36497  cdlemk33N  36691  cdlemk56  36753  dihord11b  37004  dihord2pre  37007  dihord4  37040  fourierdlem77  40880
  Copyright terms: Public domain W3C validator