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

Theorem simpl11 1249
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 1192 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜑)
213ad2antl1 1186 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  pythagtriplem4  16857  tsmsxp  24163  nolt02o  27740  nogt01o  27741  cofsslt  27952  brbtwn2  28920  ax5seg  28953  3vfriswmgr  30297  br8  35756  btwndiff  36028  ifscgr  36045  seglecgr12im  36111  lkrshp  39106  cvlcvr1  39340  atbtwn  39448  3dimlem3  39463  3dimlem3OLDN  39464  1cvratex  39475  llnmlplnN  39541  4atlem3  39598  4atlem3a  39599  4atlem11  39611  4atlem12  39614  lnatexN  39781  cdlemb  39796  paddasslem4  39825  paddasslem10  39831  pmodlem1  39848  llnexchb2lem  39870  llnexchb2  39871  arglem1N  40192  cdlemd4  40203  cdlemd9  40208  cdlemd  40209  cdleme16  40287  cdleme20  40326  cdleme21i  40337  cdleme21k  40340  cdleme27N  40371  cdleme28c  40374  cdlemefrs29bpre0  40398  cdlemefrs29clN  40401  cdlemefrs32fva  40402  cdleme41sn3a  40435  cdleme32fva  40439  cdleme40n  40470  cdlemg12e  40649  cdlemg15a  40657  cdlemg15  40658  cdlemg16ALTN  40660  cdlemg16z  40661  cdlemg20  40687  cdlemg22  40689  cdlemg29  40707  cdlemg38  40717  cdlemk33N  40911  cdlemk56  40973  dihord11b  41224  dihord2pre  41227  dihord4  41260  ismnu  44280  fourierdlem77  46198
  Copyright terms: Public domain W3C validator