Theorem simpl3r 1227

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 1185	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  tfisi  7857  offsplitfpar  8118  omopth2  8598  ltmul1a  12087  xmulasslem3  13291  xadddi2  13302  swrdsbslen  14640  swrdspsleq  14641  dvdsadd2b  16276  pockthg  16868  psgnunilem4  19445  efgred  19696  marrepeval  22458  submaeval  22477  mdetmul  22518  minmar1eval  22544  ptbasin  23474  basqtop  23608  xrsmopn  24721  nosupbnd1lem3  27636  nosupbnd1lem4  27637  nosupbnd1lem5  27638  noinfbnd1lem3  27651  noinfbnd1lem4  27652  noinfbnd1lem5  27653  precsexlem8  28105  axpasch  28745  axeuclid  28767  elwwlks2ons3im  29758  mhmimasplusg  32752  br4  35342  btwnouttr2  35608  trisegint  35614  cgrxfr  35641  lineext  35662  btwnconn1lem13  35685  btwnconn1lem14  35686  btwnconn3  35689  brsegle  35694  brsegle2  35695  segleantisym  35701  outsideofeu  35717  lineunray  35733  lineelsb2  35734  cvrcmp  38744  atcvrj2b  38894  3dimlem3  38923  3dimlem3OLDN  38924  3dim3  38931  ps-1  38939  ps-2  38940  lplnnle2at  39003  2llnm3N  39031  4atlem0a  39055  4atlem3  39058  4atlem3a  39059  lnatexN  39241  paddasslem8  39289  paddasslem9  39290  paddasslem10  39291  paddasslem12  39293  paddasslem13  39294  lhpexle2lem  39471  lhpexle3  39474  lhpat3  39508  4atex  39538  trlval2  39625  trlval4  39650  cdleme16  39747  cdleme21  39799  cdleme21k  39800  cdleme27cl  39828  cdleme27N  39831  cdleme43fsv1snlem  39882  cdleme48fvg  39962  cdlemg8  40093  cdlemg15a  40117  cdlemg16z  40121  cdlemg24  40150  cdlemg38  40177  cdlemg40  40179  trlcone  40190  cdlemj2  40284  tendoid0  40287  tendoconid  40291  cdlemk34  40372  cdlemk38  40377  cdlemkid4  40396  cdlemk53  40419  tendospcanN  40485  dihvalcqpre  40697  dihmeetlem15N  40783  qirropth  42300  mzpcong  42365  jm2.26  42395  aomclem6  42455  islptre  44979  limccog  44980  limcleqr  45004  fourierdlem42  45509  elaa2  45594  itsclc0b  47817