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  7795  offsplitfpar  8055  omopth2  8505  ltmul1a  11976  xmulasslem3  13191  xadddi2  13202  swrdsbslen  14578  swrdspsleq  14579  dvdsadd2b  16223  pockthg  16824  psgnunilem4  19415  efgred  19666  marrepeval  22484  submaeval  22503  mdetmul  22544  minmar1eval  22570  ptbasin  23498  basqtop  23632  xrsmopn  24734  nosupbnd1lem3  27655  nosupbnd1lem4  27656  nosupbnd1lem5  27657  noinfbnd1lem3  27670  noinfbnd1lem4  27671  noinfbnd1lem5  27672  precsexlem8  28158  axpasch  28926  axeuclid  28948  elwwlks2ons3im  29939  mhmimasplusg  33026  br4  35809  btwnouttr2  36073  trisegint  36079  cgrxfr  36106  lineext  36127  btwnconn1lem13  36150  btwnconn1lem14  36151  btwnconn3  36154  brsegle  36159  brsegle2  36160  segleantisym  36166  outsideofeu  36182  lineunray  36198  lineelsb2  36199  cvrcmp  39388  atcvrj2b  39537  3dimlem3  39566  3dimlem3OLDN  39567  3dim3  39574  ps-1  39582  ps-2  39583  lplnnle2at  39646  2llnm3N  39674  4atlem0a  39698  4atlem3  39701  4atlem3a  39702  lnatexN  39884  paddasslem8  39932  paddasslem9  39933  paddasslem10  39934  paddasslem12  39936  paddasslem13  39937  lhpexle2lem  40114  lhpexle3  40117  lhpat3  40151  4atex  40181  trlval2  40268  trlval4  40293  cdleme16  40390  cdleme21  40442  cdleme21k  40443  cdleme27cl  40471  cdleme27N  40474  cdleme43fsv1snlem  40525  cdleme48fvg  40605  cdlemg8  40736  cdlemg15a  40760  cdlemg16z  40764  cdlemg24  40793  cdlemg38  40820  cdlemg40  40822  trlcone  40833  cdlemj2  40927  tendoid0  40930  tendoconid  40934  cdlemk34  41015  cdlemk38  41020  cdlemkid4  41039  cdlemk53  41062  tendospcanN  41128  dihvalcqpre  41340  dihmeetlem15N  41426  qirropth  43006  mzpcong  43070  jm2.26  43100  aomclem6  43157  islptre  45724  limccog  45725  limcleqr  45747  fourierdlem42  46252  elaa2  46337  submodneaddmod  47456  itsclc0b  48878