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  7810  offsplitfpar  8069  omopth2  8519  ltmul1a  12004  xmulasslem3  13238  xadddi2  13249  swrdsbslen  14627  swrdspsleq  14628  dvdsadd2b  16275  pockthg  16877  psgnunilem4  19472  efgred  19723  marrepeval  22528  submaeval  22547  mdetmul  22588  minmar1eval  22614  ptbasin  23542  basqtop  23676  xrsmopn  24778  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  precsexlem8  28206  axpasch  29010  axeuclid  29032  elwwlks2ons3im  30022  mhmimasplusg  33098  br4  35940  btwnouttr2  36204  trisegint  36210  cgrxfr  36237  lineext  36258  btwnconn1lem13  36281  btwnconn1lem14  36282  btwnconn3  36285  brsegle  36290  brsegle2  36291  segleantisym  36297  outsideofeu  36313  lineunray  36329  lineelsb2  36330  cvrcmp  39729  atcvrj2b  39878  3dimlem3  39907  3dimlem3OLDN  39908  3dim3  39915  ps-1  39923  ps-2  39924  lplnnle2at  39987  2llnm3N  40015  4atlem0a  40039  4atlem3  40042  4atlem3a  40043  lnatexN  40225  paddasslem8  40273  paddasslem9  40274  paddasslem10  40275  paddasslem12  40277  paddasslem13  40278  lhpexle2lem  40455  lhpexle3  40458  lhpat3  40492  4atex  40522  trlval2  40609  trlval4  40634  cdleme16  40731  cdleme21  40783  cdleme21k  40784  cdleme27cl  40812  cdleme27N  40815  cdleme43fsv1snlem  40866  cdleme48fvg  40946  cdlemg8  41077  cdlemg15a  41101  cdlemg16z  41105  cdlemg24  41134  cdlemg38  41161  cdlemg40  41163  trlcone  41174  cdlemj2  41268  tendoid0  41271  tendoconid  41275  cdlemk34  41356  cdlemk38  41361  cdlemkid4  41380  cdlemk53  41403  tendospcanN  41469  dihvalcqpre  41681  dihmeetlem15N  41767  qirropth  43336  mzpcong  43400  jm2.26  43430  aomclem6  43487  islptre  46049  limccog  46050  limcleqr  46072  fourierdlem42  46577  elaa2  46662  submodneaddmod  47805  itsclc0b  49248