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

Theorem simpl3r 1221
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 1179 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 1081
This theorem is referenced by:  tfisi  7562  offsplitfpar  7804  omopth2  8199  ltmul1a  11477  xmulasslem3  12667  xadddi2  12678  swrdsbslen  14014  swrdspsleq  14015  dvdsadd2b  15644  pockthg  16230  psgnunilem4  18554  efgred  18803  marrepeval  21100  submaeval  21119  mdetmul  21160  minmar1eval  21186  ptbasin  22113  basqtop  22247  xrsmopn  23347  axpasch  26654  axeuclid  26676  elwwlks2ons3im  27660  br4  32891  nosupbnd1lem3  33107  nosupbnd1lem4  33108  nosupbnd1lem5  33109  btwnouttr2  33380  trisegint  33386  cgrxfr  33413  lineext  33434  btwnconn1lem13  33457  btwnconn1lem14  33458  btwnconn3  33461  brsegle  33466  brsegle2  33467  segleantisym  33473  outsideofeu  33489  lineunray  33505  lineelsb2  33506  cvrcmp  36299  atcvrj2b  36448  3dimlem3  36477  3dimlem3OLDN  36478  3dim3  36485  ps-1  36493  ps-2  36494  lplnnle2at  36557  2llnm3N  36585  4atlem0a  36609  4atlem3  36612  4atlem3a  36613  lnatexN  36795  paddasslem8  36843  paddasslem9  36844  paddasslem10  36845  paddasslem12  36847  paddasslem13  36848  lhpexle2lem  37025  lhpexle3  37028  lhpat3  37062  4atex  37092  trlval2  37179  trlval4  37204  cdleme16  37301  cdleme21  37353  cdleme21k  37354  cdleme27cl  37382  cdleme27N  37385  cdleme43fsv1snlem  37436  cdleme48fvg  37516  cdlemg8  37647  cdlemg15a  37671  cdlemg16z  37675  cdlemg24  37704  cdlemg38  37731  cdlemg40  37733  trlcone  37744  cdlemj2  37838  tendoid0  37841  tendoconid  37845  cdlemk34  37926  cdlemk38  37931  cdlemkid4  37950  cdlemk53  37973  tendospcanN  38039  dihvalcqpre  38251  dihmeetlem15N  38337  qirropth  39383  mzpcong  39447  jm2.26  39477  aomclem6  39537  islptre  41776  limccog  41777  limcleqr  41801  fourierdlem42  42311  elaa2  42396  itsclc0b  44687
  Copyright terms: Public domain W3C validator