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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ 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 401  df-3an 1105

This theorem is used by:  tfisi  7851  offsplitfpar  8110  omopth2  8565  ltmul1a  12068  xmulasslem3  13316  xadddi2  13327  swrdsbslen  14707  swrdspsleq  14708  dvdsadd2b  16368  pockthg  16970  psgnunilem4  19571  efgred  19822  marrepeval  22729  submaeval  22748  mdetmul  22789  minmar1eval  22815  ptbasin  23743  basqtop  23877  xrsmopn  24979  nosupbnd1lem3  27883  nosupbnd1lem4  27884  nosupbnd1lem5  27885  noinfbnd1lem3  27898  noinfbnd1lem4  27899  noinfbnd1lem5  27900  precsexlem8  28416  axpasch  29300  axeuclid  29322  elwwlks2ons3im  30312  mhmimasplusg  33366  br4  36258  btwnouttr2  36522  trisegint  36528  cgrxfr  36555  lineext  36576  btwnconn1lem13  36599  btwnconn1lem14  36600  btwnconn3  36603  brsegle  36608  brsegle2  36609  segleantisym  36615  outsideofeu  36631  lineunray  36647  lineelsb2  36648  cvrcmp  40085  atcvrj2b  40234  3dimlem3  40263  3dimlem3OLDN  40264  3dim3  40271  ps-1  40279  ps-2  40280  lplnnle2at  40343  2llnm3N  40371  4atlem0a  40395  4atlem3  40398  4atlem3a  40399  lnatexN  40581  paddasslem8  40629  paddasslem9  40630  paddasslem10  40631  paddasslem12  40633  paddasslem13  40634  lhpexle2lem  40811  lhpexle3  40814  lhpat3  40848  4atex  40878  trlval2  40965  trlval4  40990  cdleme16  41087  cdleme21  41139  cdleme21k  41140  cdleme27cl  41168  cdleme27N  41171  cdleme43fsv1snlem  41222  cdleme48fvg  41302  cdlemg8  41433  cdlemg15a  41457  cdlemg16z  41461  cdlemg24  41490  cdlemg38  41517  cdlemg40  41519  trlcone  41530  cdlemj2  41624  tendoid0  41627  tendoconid  41631  cdlemk34  41712  cdlemk38  41717  cdlemkid4  41736  cdlemk53  41759  tendospcanN  41825  dihvalcqpre  42037  dihmeetlem15N  42123  qirropth  43663  mzpcong  43727  jm2.26  43757  aomclem6  43814  islptre  46363  limccog  46364  limcleqr  46386  fourierdlem42  46891  elaa2  46976  submodneaddmod  48122  itsclc0b  49580