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

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  tfisi  7850  offsplitfpar  8107  omopth2  8586  ltmul1a  12067  xmulasslem3  13269  xadddi2  13280  swrdsbslen  14618  swrdspsleq  14619  dvdsadd2b  16253  pockthg  16843  psgnunilem4  19406  efgred  19657  marrepeval  22285  submaeval  22304  mdetmul  22345  minmar1eval  22371  ptbasin  23301  basqtop  23435  xrsmopn  24548  nosupbnd1lem3  27449  nosupbnd1lem4  27450  nosupbnd1lem5  27451  noinfbnd1lem3  27464  noinfbnd1lem4  27465  noinfbnd1lem5  27466  precsexlem8  27899  axpasch  28466  axeuclid  28488  elwwlks2ons3im  29475  mhmimasplusg  32466  br4  35032  btwnouttr2  35298  trisegint  35304  cgrxfr  35331  lineext  35352  btwnconn1lem13  35375  btwnconn1lem14  35376  btwnconn3  35379  brsegle  35384  brsegle2  35385  segleantisym  35391  outsideofeu  35407  lineunray  35423  lineelsb2  35424  cvrcmp  38456  atcvrj2b  38606  3dimlem3  38635  3dimlem3OLDN  38636  3dim3  38643  ps-1  38651  ps-2  38652  lplnnle2at  38715  2llnm3N  38743  4atlem0a  38767  4atlem3  38770  4atlem3a  38771  lnatexN  38953  paddasslem8  39001  paddasslem9  39002  paddasslem10  39003  paddasslem12  39005  paddasslem13  39006  lhpexle2lem  39183  lhpexle3  39186  lhpat3  39220  4atex  39250  trlval2  39337  trlval4  39362  cdleme16  39459  cdleme21  39511  cdleme21k  39512  cdleme27cl  39540  cdleme27N  39543  cdleme43fsv1snlem  39594  cdleme48fvg  39674  cdlemg8  39805  cdlemg15a  39829  cdlemg16z  39833  cdlemg24  39862  cdlemg38  39889  cdlemg40  39891  trlcone  39902  cdlemj2  39996  tendoid0  39999  tendoconid  40003  cdlemk34  40084  cdlemk38  40089  cdlemkid4  40108  cdlemk53  40131  tendospcanN  40197  dihvalcqpre  40409  dihmeetlem15N  40495  qirropth  41948  mzpcong  42013  jm2.26  42043  aomclem6  42103  islptre  44633  limccog  44634  limcleqr  44658  fourierdlem42  45163  elaa2  45248  itsclc0b  47545