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

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

Proof of Theorem simpl3r
StepHypRef Expression
1 simplr 765 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl3 1181 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  tfisi  7566  offsplitfpar  7811  omopth2  8205  ltmul1a  11483  xmulasslem3  12674  xadddi2  12685  swrdsbslen  14021  swrdspsleq  14022  dvdsadd2b  15651  pockthg  16237  psgnunilem4  18561  efgred  18810  marrepeval  21107  submaeval  21126  mdetmul  21167  minmar1eval  21193  ptbasin  22120  basqtop  22254  xrsmopn  23354  axpasch  26660  axeuclid  26682  elwwlks2ons3im  27666  br4  32897  nosupbnd1lem3  33113  nosupbnd1lem4  33114  nosupbnd1lem5  33115  btwnouttr2  33386  trisegint  33392  cgrxfr  33419  lineext  33440  btwnconn1lem13  33463  btwnconn1lem14  33464  btwnconn3  33467  brsegle  33472  brsegle2  33473  segleantisym  33479  outsideofeu  33495  lineunray  33511  lineelsb2  33512  cvrcmp  36305  atcvrj2b  36454  3dimlem3  36483  3dimlem3OLDN  36484  3dim3  36491  ps-1  36499  ps-2  36500  lplnnle2at  36563  2llnm3N  36591  4atlem0a  36615  4atlem3  36618  4atlem3a  36619  lnatexN  36801  paddasslem8  36849  paddasslem9  36850  paddasslem10  36851  paddasslem12  36853  paddasslem13  36854  lhpexle2lem  37031  lhpexle3  37034  lhpat3  37068  4atex  37098  trlval2  37185  trlval4  37210  cdleme16  37307  cdleme21  37359  cdleme21k  37360  cdleme27cl  37388  cdleme27N  37391  cdleme43fsv1snlem  37442  cdleme48fvg  37522  cdlemg8  37653  cdlemg15a  37677  cdlemg16z  37681  cdlemg24  37710  cdlemg38  37737  cdlemg40  37739  trlcone  37750  cdlemj2  37844  tendoid0  37847  tendoconid  37851  cdlemk34  37932  cdlemk38  37937  cdlemkid4  37956  cdlemk53  37979  tendospcanN  38045  dihvalcqpre  38257  dihmeetlem15N  38343  qirropth  39389  mzpcong  39453  jm2.26  39483  aomclem6  39543  islptre  41784  limccog  41785  limcleqr  41809  fourierdlem42  42319  elaa2  42404  itsclc0b  44661
  Copyright terms: Public domain W3C validator