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  7859  offsplitfpar  8119  omopth2  8576  ltmul1a  12147  xmulasslem3  13397  xadddi2  13408  swrdsbslen  14794  swrdspsleq  14795  dvdsadd2b  16456  pockthg  17064  psgnunilem4  19691  efgred  19942  marrepeval  22858  submaeval  22877  mdetmul  22918  minmar1eval  22944  ptbasin  23876  basqtop  24010  xrsmopn  25112  nosupbnd1lem3  28049  nosupbnd1lem4  28050  nosupbnd1lem5  28051  noinfbnd1lem3  28064  noinfbnd1lem4  28065  noinfbnd1lem5  28066  precsexlem8  28582  axpasch  29501  axeuclid  29523  elwwlks2ons3im  30525  mhmimasplusg  33580  br4  36492  btwnouttr2  36757  trisegint  36763  cgrxfr  36790  lineext  36811  btwnconn1lem13  36834  btwnconn1lem14  36835  btwnconn3  36838  brsegle  36843  brsegle2  36844  segleantisym  36850  outsideofeu  36866  lineunray  36882  lineelsb2  36883  cvrcmp  40308  atcvrj2b  40457  3dimlem3  40486  3dimlem3OLDN  40487  3dim3  40494  ps-1  40502  ps-2  40503  lplnnle2at  40566  2llnm3N  40594  4atlem0a  40618  4atlem3  40621  4atlem3a  40622  lnatexN  40804  paddasslem8  40852  paddasslem9  40853  paddasslem10  40854  paddasslem12  40856  paddasslem13  40857  lhpexle2lem  41034  lhpexle3  41037  lhpat3  41071  4atex  41101  trlval2  41188  trlval4  41213  cdleme16  41310  cdleme21  41362  cdleme21k  41363  cdleme27cl  41391  cdleme27N  41394  cdleme43fsv1snlem  41445  cdleme48fvg  41525  cdlemg8  41656  cdlemg15a  41680  cdlemg16z  41684  cdlemg24  41713  cdlemg38  41740  cdlemg40  41742  trlcone  41753  cdlemj2  41847  tendoid0  41850  tendoconid  41854  cdlemk34  41935  cdlemk38  41940  cdlemkid4  41959  cdlemk53  41982  tendospcanN  42048  dihvalcqpre  42260  dihmeetlem15N  42346  qirropth  43868  mzpcong  43932  jm2.26  43962  aomclem6  44019  islptre  46575  limccog  46576  limcleqr  46598  fourierdlem42  47103  elaa2  47188  submodneaddmod  48371  itsclc0b  49828