Theorem simpl3r 1236

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  tfisi  7806  offsplitfpar  8065  omopth2  8516  ltmul1a  12002  xmulasslem3  13236  xadddi2  13247  swrdsbslen  14625  swrdspsleq  14626  dvdsadd2b  16273  pockthg  16875  psgnunilem4  19470  efgred  19721  marrepeval  22553  submaeval  22572  mdetmul  22613  minmar1eval  22639  ptbasin  23567  basqtop  23701  xrsmopn  24803  nosupbnd1lem3  27699  nosupbnd1lem4  27700  nosupbnd1lem5  27701  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  precsexlem8  28231  axpasch  29035  axeuclid  29057  elwwlks2ons3im  30047  mhmimasplusg  33124  br4  35993  btwnouttr2  36257  trisegint  36263  cgrxfr  36290  lineext  36311  btwnconn1lem13  36334  btwnconn1lem14  36335  btwnconn3  36338  brsegle  36343  brsegle2  36344  segleantisym  36350  outsideofeu  36366  lineunray  36382  lineelsb2  36383  cvrcmp  39782  atcvrj2b  39931  3dimlem3  39960  3dimlem3OLDN  39961  3dim3  39968  ps-1  39976  ps-2  39977  lplnnle2at  40040  2llnm3N  40068  4atlem0a  40092  4atlem3  40095  4atlem3a  40096  lnatexN  40278  paddasslem8  40326  paddasslem9  40327  paddasslem10  40328  paddasslem12  40330  paddasslem13  40331  lhpexle2lem  40508  lhpexle3  40511  lhpat3  40545  4atex  40575  trlval2  40662  trlval4  40687  cdleme16  40784  cdleme21  40836  cdleme21k  40837  cdleme27cl  40865  cdleme27N  40868  cdleme43fsv1snlem  40919  cdleme48fvg  40999  cdlemg8  41130  cdlemg15a  41154  cdlemg16z  41158  cdlemg24  41187  cdlemg38  41214  cdlemg40  41216  trlcone  41227  cdlemj2  41321  tendoid0  41324  tendoconid  41328  cdlemk34  41409  cdlemk38  41414  cdlemkid4  41433  cdlemk53  41456  tendospcanN  41522  dihvalcqpre  41734  dihmeetlem15N  41820  qirropth  43360  mzpcong  43424  jm2.26  43454  aomclem6  43511  islptre  46071  limccog  46072  limcleqr  46094  fourierdlem42  46599  elaa2  46684  submodneaddmod  47827  itsclc0b  49270