Theorem simpl3r 1246

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

Step	Hyp	Ref	Expression
1		simplr 780	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl3 1204	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  tfisi  7843  offsplitfpar  8102  omopth2  8557  ltmul1a  12055  xmulasslem3  13303  xadddi2  13314  swrdsbslen  14692  swrdspsleq  14693  dvdsadd2b  16354  pockthg  16956  psgnunilem4  19558  efgred  19809  marrepeval  22681  submaeval  22700  mdetmul  22741  minmar1eval  22767  ptbasin  23695  basqtop  23829  xrsmopn  24931  nosupbnd1lem3  27832  nosupbnd1lem4  27833  nosupbnd1lem5  27834  noinfbnd1lem3  27847  noinfbnd1lem4  27848  noinfbnd1lem5  27849  precsexlem8  28365  axpasch  29200  axeuclid  29222  elwwlks2ons3im  30212  mhmimasplusg  33270  br4  36121  btwnouttr2  36385  trisegint  36391  cgrxfr  36418  lineext  36439  btwnconn1lem13  36462  btwnconn1lem14  36463  btwnconn3  36466  brsegle  36471  brsegle2  36472  segleantisym  36478  outsideofeu  36494  lineunray  36510  lineelsb2  36511  cvrcmp  39919  atcvrj2b  40068  3dimlem3  40097  3dimlem3OLDN  40098  3dim3  40105  ps-1  40113  ps-2  40114  lplnnle2at  40177  2llnm3N  40205  4atlem0a  40229  4atlem3  40232  4atlem3a  40233  lnatexN  40415  paddasslem8  40463  paddasslem9  40464  paddasslem10  40465  paddasslem12  40467  paddasslem13  40468  lhpexle2lem  40645  lhpexle3  40648  lhpat3  40682  4atex  40712  trlval2  40799  trlval4  40824  cdleme16  40921  cdleme21  40973  cdleme21k  40974  cdleme27cl  41002  cdleme27N  41005  cdleme43fsv1snlem  41056  cdleme48fvg  41136  cdlemg8  41267  cdlemg15a  41291  cdlemg16z  41295  cdlemg24  41324  cdlemg38  41351  cdlemg40  41353  trlcone  41364  cdlemj2  41458  tendoid0  41461  tendoconid  41465  cdlemk34  41546  cdlemk38  41551  cdlemkid4  41570  cdlemk53  41593  tendospcanN  41659  dihvalcqpre  41871  dihmeetlem15N  41957  qirropth  43497  mzpcong  43561  jm2.26  43591  aomclem6  43648  islptre  46193  limccog  46194  limcleqr  46216  fourierdlem42  46721  elaa2  46806  submodneaddmod  47949  itsclc0b  49403