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

Theorem simpl3r 1288
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 752 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl3 1202 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  tfisi  7208  omopth2  7821  ltmul1a  11077  xmulasslem3  12320  xadddi2  12331  swrdsbslen  13656  swrdspsleq  13657  dvdsadd2b  15236  pockthg  15816  psgnunilem4  18123  efgred  18367  marrepeval  20586  submaeval  20605  mdetmul  20646  minmar1eval  20672  ptbasin  21600  basqtop  21734  xrsmopn  22834  axpasch  26041  axeuclid  26063  elwwlks2ons3im  27100  br4  31985  nosupbnd1lem3  32192  nosupbnd1lem4  32193  nosupbnd1lem5  32194  btwnouttr2  32465  trisegint  32471  cgrxfr  32498  lineext  32519  btwnconn1lem13  32542  btwnconn1lem14  32543  btwnconn3  32546  brsegle  32551  brsegle2  32552  segleantisym  32558  outsideofeu  32574  lineunray  32590  lineelsb2  32591  cvrcmp  35091  atcvrj2b  35240  3dimlem3  35269  3dimlem3OLDN  35270  3dim3  35277  ps-1  35285  ps-2  35286  lplnnle2at  35349  2llnm3N  35377  4atlem0a  35401  4atlem3  35404  4atlem3a  35405  lnatexN  35587  paddasslem8  35635  paddasslem9  35636  paddasslem10  35637  paddasslem12  35639  paddasslem13  35640  lhpexle2lem  35817  lhpexle3  35820  lhpat3  35854  4atex  35884  trlval2  35972  trlval4  35997  cdleme16  36094  cdleme21  36146  cdleme21k  36147  cdleme27cl  36175  cdleme27N  36178  cdleme43fsv1snlem  36229  cdleme48fvg  36309  cdlemg8  36440  cdlemg15a  36464  cdlemg16z  36468  cdlemg24  36497  cdlemg38  36524  cdlemg40  36526  trlcone  36537  cdlemj2  36631  tendoid0  36634  tendoconid  36638  cdlemk34  36719  cdlemk38  36724  cdlemkid4  36743  cdlemk53  36766  tendospcanN  36833  dihvalcqpre  37045  dihmeetlem15N  37131  qirropth  37999  mzpcong  38065  jm2.26  38095  aomclem6  38155  islptre  40366  limccog  40367  limcleqr  40391  fourierdlem42  40880  elaa2  40965
  Copyright terms: Public domain W3C validator