Theorem simpl3r 1231

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

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

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 1089

This theorem is referenced by:  tfisi  7811  offsplitfpar  8071  omopth2  8521  ltmul1a  12002  xmulasslem3  13213  xadddi2  13224  swrdsbslen  14600  swrdspsleq  14601  dvdsadd2b  16245  pockthg  16846  psgnunilem4  19438  efgred  19689  marrepeval  22519  submaeval  22538  mdetmul  22579  minmar1eval  22605  ptbasin  23533  basqtop  23667  xrsmopn  24769  nosupbnd1lem3  27690  nosupbnd1lem4  27691  nosupbnd1lem5  27692  noinfbnd1lem3  27705  noinfbnd1lem4  27706  noinfbnd1lem5  27707  precsexlem8  28222  axpasch  29026  axeuclid  29048  elwwlks2ons3im  30039  mhmimasplusg  33130  br4  35971  btwnouttr2  36235  trisegint  36241  cgrxfr  36268  lineext  36289  btwnconn1lem13  36312  btwnconn1lem14  36313  btwnconn3  36316  brsegle  36321  brsegle2  36322  segleantisym  36328  outsideofeu  36344  lineunray  36360  lineelsb2  36361  cvrcmp  39653  atcvrj2b  39802  3dimlem3  39831  3dimlem3OLDN  39832  3dim3  39839  ps-1  39847  ps-2  39848  lplnnle2at  39911  2llnm3N  39939  4atlem0a  39963  4atlem3  39966  4atlem3a  39967  lnatexN  40149  paddasslem8  40197  paddasslem9  40198  paddasslem10  40199  paddasslem12  40201  paddasslem13  40202  lhpexle2lem  40379  lhpexle3  40382  lhpat3  40416  4atex  40446  trlval2  40533  trlval4  40558  cdleme16  40655  cdleme21  40707  cdleme21k  40708  cdleme27cl  40736  cdleme27N  40739  cdleme43fsv1snlem  40790  cdleme48fvg  40870  cdlemg8  41001  cdlemg15a  41025  cdlemg16z  41029  cdlemg24  41058  cdlemg38  41085  cdlemg40  41087  trlcone  41098  cdlemj2  41192  tendoid0  41195  tendoconid  41199  cdlemk34  41280  cdlemk38  41285  cdlemkid4  41304  cdlemk53  41327  tendospcanN  41393  dihvalcqpre  41605  dihmeetlem15N  41691  qirropth  43259  mzpcong  43323  jm2.26  43353  aomclem6  43410  islptre  45973  limccog  45974  limcleqr  45996  fourierdlem42  46501  elaa2  46586  submodneaddmod  47705  itsclc0b  49126