Theorem simpl3r 1242

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  tfisi  7835  offsplitfpar  8093  omopth2  8548  ltmul1a  12037  xmulasslem3  13286  xadddi2  13297  swrdsbslen  14675  swrdspsleq  14676  dvdsadd2b  16323  pockthg  16925  psgnunilem4  19520  efgred  19771  marrepeval  22603  submaeval  22622  mdetmul  22663  minmar1eval  22689  ptbasin  23617  basqtop  23751  xrsmopn  24853  nosupbnd1lem3  27751  nosupbnd1lem4  27752  nosupbnd1lem5  27753  noinfbnd1lem3  27766  noinfbnd1lem4  27767  noinfbnd1lem5  27768  precsexlem8  28284  axpasch  29088  axeuclid  29110  elwwlks2ons3im  30100  mhmimasplusg  33177  br4  36072  btwnouttr2  36336  trisegint  36342  cgrxfr  36369  lineext  36390  btwnconn1lem13  36413  btwnconn1lem14  36414  btwnconn3  36417  brsegle  36422  brsegle2  36423  segleantisym  36429  outsideofeu  36445  lineunray  36461  lineelsb2  36462  cvrcmp  39871  atcvrj2b  40020  3dimlem3  40049  3dimlem3OLDN  40050  3dim3  40057  ps-1  40065  ps-2  40066  lplnnle2at  40129  2llnm3N  40157  4atlem0a  40181  4atlem3  40184  4atlem3a  40185  lnatexN  40367  paddasslem8  40415  paddasslem9  40416  paddasslem10  40417  paddasslem12  40419  paddasslem13  40420  lhpexle2lem  40597  lhpexle3  40600  lhpat3  40634  4atex  40664  trlval2  40751  trlval4  40776  cdleme16  40873  cdleme21  40925  cdleme21k  40926  cdleme27cl  40954  cdleme27N  40957  cdleme43fsv1snlem  41008  cdleme48fvg  41088  cdlemg8  41219  cdlemg15a  41243  cdlemg16z  41247  cdlemg24  41276  cdlemg38  41303  cdlemg40  41305  trlcone  41316  cdlemj2  41410  tendoid0  41413  tendoconid  41417  cdlemk34  41498  cdlemk38  41503  cdlemkid4  41522  cdlemk53  41545  tendospcanN  41611  dihvalcqpre  41823  dihmeetlem15N  41909  qirropth  43449  mzpcong  43513  jm2.26  43543  aomclem6  43600  islptre  46159  limccog  46160  limcleqr  46182  fourierdlem42  46687  elaa2  46772  submodneaddmod  47915  itsclc0b  49358