Theorem simpl3r 1230

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 768	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl3 1188	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfisi  7795  offsplitfpar  8055  omopth2  8505  ltmul1a  11977  xmulasslem3  13187  xadddi2  13198  swrdsbslen  14574  swrdspsleq  14575  dvdsadd2b  16219  pockthg  16820  psgnunilem4  19411  efgred  19662  marrepeval  22479  submaeval  22498  mdetmul  22539  minmar1eval  22565  ptbasin  23493  basqtop  23627  xrsmopn  24729  nosupbnd1lem3  27650  nosupbnd1lem4  27651  nosupbnd1lem5  27652  noinfbnd1lem3  27665  noinfbnd1lem4  27666  noinfbnd1lem5  27667  precsexlem8  28153  axpasch  28921  axeuclid  28943  elwwlks2ons3im  29934  mhmimasplusg  33026  br4  35823  btwnouttr2  36087  trisegint  36093  cgrxfr  36120  lineext  36141  btwnconn1lem13  36164  btwnconn1lem14  36165  btwnconn3  36168  brsegle  36173  brsegle2  36174  segleantisym  36180  outsideofeu  36196  lineunray  36212  lineelsb2  36213  cvrcmp  39402  atcvrj2b  39551  3dimlem3  39580  3dimlem3OLDN  39581  3dim3  39588  ps-1  39596  ps-2  39597  lplnnle2at  39660  2llnm3N  39688  4atlem0a  39712  4atlem3  39715  4atlem3a  39716  lnatexN  39898  paddasslem8  39946  paddasslem9  39947  paddasslem10  39948  paddasslem12  39950  paddasslem13  39951  lhpexle2lem  40128  lhpexle3  40131  lhpat3  40165  4atex  40195  trlval2  40282  trlval4  40307  cdleme16  40404  cdleme21  40456  cdleme21k  40457  cdleme27cl  40485  cdleme27N  40488  cdleme43fsv1snlem  40539  cdleme48fvg  40619  cdlemg8  40750  cdlemg15a  40774  cdlemg16z  40778  cdlemg24  40807  cdlemg38  40834  cdlemg40  40836  trlcone  40847  cdlemj2  40941  tendoid0  40944  tendoconid  40948  cdlemk34  41029  cdlemk38  41034  cdlemkid4  41053  cdlemk53  41076  tendospcanN  41142  dihvalcqpre  41354  dihmeetlem15N  41440  qirropth  43025  mzpcong  43089  jm2.26  43119  aomclem6  43176  islptre  45743  limccog  45744  limcleqr  45766  fourierdlem42  46271  elaa2  46356  submodneaddmod  47475  itsclc0b  48897