Theorem simpl3r 1230

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

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

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 1088

This theorem is referenced by:  tfisi  7835  offsplitfpar  8098  omopth2  8548  ltmul1a  12031  xmulasslem3  13246  xadddi2  13257  swrdsbslen  14629  swrdspsleq  14630  dvdsadd2b  16276  pockthg  16877  psgnunilem4  19427  efgred  19678  marrepeval  22450  submaeval  22469  mdetmul  22510  minmar1eval  22536  ptbasin  23464  basqtop  23598  xrsmopn  24701  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  precsexlem8  28116  axpasch  28868  axeuclid  28890  elwwlks2ons3im  29884  mhmimasplusg  32979  br4  35745  btwnouttr2  36010  trisegint  36016  cgrxfr  36043  lineext  36064  btwnconn1lem13  36087  btwnconn1lem14  36088  btwnconn3  36091  brsegle  36096  brsegle2  36097  segleantisym  36103  outsideofeu  36119  lineunray  36135  lineelsb2  36136  cvrcmp  39276  atcvrj2b  39426  3dimlem3  39455  3dimlem3OLDN  39456  3dim3  39463  ps-1  39471  ps-2  39472  lplnnle2at  39535  2llnm3N  39563  4atlem0a  39587  4atlem3  39590  4atlem3a  39591  lnatexN  39773  paddasslem8  39821  paddasslem9  39822  paddasslem10  39823  paddasslem12  39825  paddasslem13  39826  lhpexle2lem  40003  lhpexle3  40006  lhpat3  40040  4atex  40070  trlval2  40157  trlval4  40182  cdleme16  40279  cdleme21  40331  cdleme21k  40332  cdleme27cl  40360  cdleme27N  40363  cdleme43fsv1snlem  40414  cdleme48fvg  40494  cdlemg8  40625  cdlemg15a  40649  cdlemg16z  40653  cdlemg24  40682  cdlemg38  40709  cdlemg40  40711  trlcone  40722  cdlemj2  40816  tendoid0  40819  tendoconid  40823  cdlemk34  40904  cdlemk38  40909  cdlemkid4  40928  cdlemk53  40951  tendospcanN  41017  dihvalcqpre  41229  dihmeetlem15N  41315  qirropth  42896  mzpcong  42961  jm2.26  42991  aomclem6  43048  islptre  45617  limccog  45618  limcleqr  45642  fourierdlem42  46147  elaa2  46232  submodneaddmod  47352  itsclc0b  48761