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

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

Proof of Theorem simpl12
StepHypRef Expression
1 simpl2 1230 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl1 1201 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  pythagtriplem4  15746  pmatcollpw1lem1  20801  pmatcollpw1  20803  mp2pm2mplem2  20834  brbtwn2  26005  ax5seg  26038  3vfriswmgr  27453  br8  31974  nolt02o  32172  ifscgr  32478  seglecgr12im  32544  lkrshp  34913  atlatle  35128  cvlcvr1  35147  atbtwn  35253  3dimlem3  35268  3dimlem3OLDN  35269  1cvratex  35280  llnmlplnN  35346  4atlem3  35403  4atlem3a  35404  4atlem11  35416  4atlem12  35419  cdlemb  35601  paddasslem4  35630  paddasslem10  35636  pmodlem1  35653  llnexchb2lem  35675  arglem1N  35998  cdlemd4  36009  cdlemd  36015  cdleme16  36093  cdleme20  36132  cdleme21k  36146  cdleme22cN  36150  cdleme27N  36177  cdleme28c  36180  cdleme29ex  36182  cdleme32fva  36245  cdleme40n  36276  cdlemg15a  36463  cdlemg15  36464  cdlemg16ALTN  36466  cdlemg16z  36467  cdlemg20  36493  cdlemg22  36495  cdlemg29  36513  cdlemg38  36523  cdlemk33N  36717  cdlemk56  36779  fourierdlem77  40921
  Copyright terms: Public domain W3C validator