Theorem simpl3r 1248

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfisi  7864  offsplitfpar  8123  omopth2  8578  ltmul1a  12082  xmulasslem3  13330  xadddi2  13341  swrdsbslen  14726  swrdspsleq  14727  dvdsadd2b  16389  pockthg  16991  psgnunilem4  19598  efgred  19849  marrepeval  22757  submaeval  22776  mdetmul  22817  minmar1eval  22843  ptbasin  23771  basqtop  23905  xrsmopn  25007  nosupbnd1lem3  27911  nosupbnd1lem4  27912  nosupbnd1lem5  27913  noinfbnd1lem3  27926  noinfbnd1lem4  27927  noinfbnd1lem5  27928  precsexlem8  28444  axpasch  29328  axeuclid  29350  elwwlks2ons3im  30340  mhmimasplusg  33388  br4  36271  btwnouttr2  36535  trisegint  36541  cgrxfr  36568  lineext  36589  btwnconn1lem13  36612  btwnconn1lem14  36613  btwnconn3  36616  brsegle  36621  brsegle2  36622  segleantisym  36628  outsideofeu  36644  lineunray  36660  lineelsb2  36661  cvrcmp  40098  atcvrj2b  40247  3dimlem3  40276  3dimlem3OLDN  40277  3dim3  40284  ps-1  40292  ps-2  40293  lplnnle2at  40356  2llnm3N  40384  4atlem0a  40408  4atlem3  40411  4atlem3a  40412  lnatexN  40594  paddasslem8  40642  paddasslem9  40643  paddasslem10  40644  paddasslem12  40646  paddasslem13  40647  lhpexle2lem  40824  lhpexle3  40827  lhpat3  40861  4atex  40891  trlval2  40978  trlval4  41003  cdleme16  41100  cdleme21  41152  cdleme21k  41153  cdleme27cl  41181  cdleme27N  41184  cdleme43fsv1snlem  41235  cdleme48fvg  41315  cdlemg8  41446  cdlemg15a  41470  cdlemg16z  41474  cdlemg24  41503  cdlemg38  41530  cdlemg40  41532  trlcone  41543  cdlemj2  41637  tendoid0  41640  tendoconid  41644  cdlemk34  41725  cdlemk38  41730  cdlemkid4  41749  cdlemk53  41772  tendospcanN  41838  dihvalcqpre  42050  dihmeetlem15N  42136  qirropth  43676  mzpcong  43740  jm2.26  43770  aomclem6  43827  islptre  46376  limccog  46377  limcleqr  46399  fourierdlem42  46904  elaa2  46989  submodneaddmod  48135  itsclc0b  49593