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

Theorem simpl11 1245
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 1188 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜑)
213ad2antl1 1182 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:  pythagtriplem4  16149  tsmsxp  22763  brbtwn2  26702  ax5seg  26735  3vfriswmgr  28066  br8  33100  nolt02o  33307  btwndiff  33596  ifscgr  33613  seglecgr12im  33679  lkrshp  36394  cvlcvr1  36628  atbtwn  36735  3dimlem3  36750  3dimlem3OLDN  36751  1cvratex  36762  llnmlplnN  36828  4atlem3  36885  4atlem3a  36886  4atlem11  36898  4atlem12  36901  lnatexN  37068  cdlemb  37083  paddasslem4  37112  paddasslem10  37118  pmodlem1  37135  llnexchb2lem  37157  llnexchb2  37158  arglem1N  37479  cdlemd4  37490  cdlemd9  37495  cdlemd  37496  cdleme16  37574  cdleme20  37613  cdleme21i  37624  cdleme21k  37627  cdleme27N  37658  cdleme28c  37661  cdlemefrs29bpre0  37685  cdlemefrs29clN  37688  cdlemefrs32fva  37689  cdleme41sn3a  37722  cdleme32fva  37726  cdleme40n  37757  cdlemg12e  37936  cdlemg15a  37944  cdlemg15  37945  cdlemg16ALTN  37947  cdlemg16z  37948  cdlemg20  37974  cdlemg22  37976  cdlemg29  37994  cdlemg38  38004  cdlemk33N  38198  cdlemk56  38260  dihord11b  38511  dihord2pre  38514  dihord4  38547  ismnu  40956  fourierdlem77  42812
  Copyright terms: Public domain W3C validator