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  7789  offsplitfpar  8049  omopth2  8499  ltmul1a  11967  xmulasslem3  13182  xadddi2  13193  swrdsbslen  14569  swrdspsleq  14570  dvdsadd2b  16214  pockthg  16815  psgnunilem4  19407  efgred  19658  marrepeval  22476  submaeval  22495  mdetmul  22536  minmar1eval  22562  ptbasin  23490  basqtop  23624  xrsmopn  24726  nosupbnd1lem3  27647  nosupbnd1lem4  27648  nosupbnd1lem5  27649  noinfbnd1lem3  27662  noinfbnd1lem4  27663  noinfbnd1lem5  27664  precsexlem8  28150  axpasch  28917  axeuclid  28939  elwwlks2ons3im  29930  mhmimasplusg  33014  br4  35790  btwnouttr2  36055  trisegint  36061  cgrxfr  36088  lineext  36109  btwnconn1lem13  36132  btwnconn1lem14  36133  btwnconn3  36136  brsegle  36141  brsegle2  36142  segleantisym  36148  outsideofeu  36164  lineunray  36180  lineelsb2  36181  cvrcmp  39321  atcvrj2b  39470  3dimlem3  39499  3dimlem3OLDN  39500  3dim3  39507  ps-1  39515  ps-2  39516  lplnnle2at  39579  2llnm3N  39607  4atlem0a  39631  4atlem3  39634  4atlem3a  39635  lnatexN  39817  paddasslem8  39865  paddasslem9  39866  paddasslem10  39867  paddasslem12  39869  paddasslem13  39870  lhpexle2lem  40047  lhpexle3  40050  lhpat3  40084  4atex  40114  trlval2  40201  trlval4  40226  cdleme16  40323  cdleme21  40375  cdleme21k  40376  cdleme27cl  40404  cdleme27N  40407  cdleme43fsv1snlem  40458  cdleme48fvg  40538  cdlemg8  40669  cdlemg15a  40693  cdlemg16z  40697  cdlemg24  40726  cdlemg38  40753  cdlemg40  40755  trlcone  40766  cdlemj2  40860  tendoid0  40863  tendoconid  40867  cdlemk34  40948  cdlemk38  40953  cdlemkid4  40972  cdlemk53  40995  tendospcanN  41061  dihvalcqpre  41273  dihmeetlem15N  41359  qirropth  42940  mzpcong  43004  jm2.26  43034  aomclem6  43091  islptre  45658  limccog  45659  limcleqr  45681  fourierdlem42  46186  elaa2  46271  submodneaddmod  47381  itsclc0b  48803