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

Theorem simpl11 1314
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 1227 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜑)
213ad2antl1 1200 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  pythagtriplem4  15732  tsmsxp  22179  brbtwn2  26007  ax5seg  26040  3vfriswmgr  27461  br8  31985  nolt02o  32183  btwndiff  32472  ifscgr  32489  seglecgr12im  32555  lkrshp  34915  cvlcvr1  35149  atbtwn  35255  3dimlem3  35270  3dimlem3OLDN  35271  1cvratex  35282  llnmlplnN  35348  4atlem3  35405  4atlem3a  35406  4atlem11  35418  4atlem12  35421  lnatexN  35588  cdlemb  35603  paddasslem4  35632  paddasslem10  35638  pmodlem1  35655  llnexchb2lem  35677  llnexchb2  35678  arglem1N  36000  cdlemd4  36011  cdlemd9  36016  cdlemd  36017  cdleme16  36095  cdleme20  36134  cdleme21i  36145  cdleme21k  36148  cdleme27N  36179  cdleme28c  36182  cdlemefrs29bpre0  36206  cdlemefrs29clN  36209  cdlemefrs32fva  36210  cdleme41sn3a  36243  cdleme32fva  36247  cdleme40n  36278  cdlemg12e  36457  cdlemg15a  36465  cdlemg15  36466  cdlemg16ALTN  36468  cdlemg16z  36469  cdlemg20  36495  cdlemg22  36497  cdlemg29  36515  cdlemg38  36525  cdlemk33N  36719  cdlemk56  36781  dihord11b  37033  dihord2pre  37036  dihord4  37069  fourierdlem77  40918
  Copyright terms: Public domain W3C validator