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

Theorem simpl3r 1303
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 785 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl3 1238 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  tfisi  7260  omopth2  7873  ltmul1a  11130  xmulasslem3  12323  xadddi2  12334  swrdsbslen  13660  swrdspsleq  13661  dvdsadd2b  15327  pockthg  15903  psgnunilem4  18195  efgred  18441  marrepeval  20660  submaeval  20679  mdetmul  20720  minmar1eval  20746  ptbasin  21674  basqtop  21808  xrsmopn  22908  axpasch  26126  axeuclid  26148  elwwlks2ons3im  27195  br4  32114  nosupbnd1lem3  32321  nosupbnd1lem4  32322  nosupbnd1lem5  32323  btwnouttr2  32594  trisegint  32600  cgrxfr  32627  lineext  32648  btwnconn1lem13  32671  btwnconn1lem14  32672  btwnconn3  32675  brsegle  32680  brsegle2  32681  segleantisym  32687  outsideofeu  32703  lineunray  32719  lineelsb2  32720  cvrcmp  35260  atcvrj2b  35409  3dimlem3  35438  3dimlem3OLDN  35439  3dim3  35446  ps-1  35454  ps-2  35455  lplnnle2at  35518  2llnm3N  35546  4atlem0a  35570  4atlem3  35573  4atlem3a  35574  lnatexN  35756  paddasslem8  35804  paddasslem9  35805  paddasslem10  35806  paddasslem12  35808  paddasslem13  35809  lhpexle2lem  35986  lhpexle3  35989  lhpat3  36023  4atex  36053  trlval2  36140  trlval4  36165  cdleme16  36262  cdleme21  36314  cdleme21k  36315  cdleme27cl  36343  cdleme27N  36346  cdleme43fsv1snlem  36397  cdleme48fvg  36477  cdlemg8  36608  cdlemg15a  36632  cdlemg16z  36636  cdlemg24  36665  cdlemg38  36692  cdlemg40  36694  trlcone  36705  cdlemj2  36799  tendoid0  36802  tendoconid  36806  cdlemk34  36887  cdlemk38  36892  cdlemkid4  36911  cdlemk53  36934  tendospcanN  37000  dihvalcqpre  37212  dihmeetlem15N  37298  qirropth  38174  mzpcong  38240  jm2.26  38270  aomclem6  38330  islptre  40513  limccog  40514  limcleqr  40538  fourierdlem42  41027  elaa2  41112
  Copyright terms: Public domain W3C validator