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  8120  omopth2  8575  ltmul1a  12092  xmulasslem3  13342  xadddi2  13353  swrdsbslen  14738  swrdspsleq  14739  dvdsadd2b  16402  pockthg  17004  psgnunilem4  19630  efgred  19881  marrepeval  22791  submaeval  22810  mdetmul  22851  minmar1eval  22877  ptbasin  23809  basqtop  23943  xrsmopn  25045  nosupbnd1lem3  27954  nosupbnd1lem4  27955  nosupbnd1lem5  27956  noinfbnd1lem3  27969  noinfbnd1lem4  27970  noinfbnd1lem5  27971  precsexlem8  28487  axpasch  29406  axeuclid  29428  elwwlks2ons3im  30430  mhmimasplusg  33485  br4  36345  btwnouttr2  36610  trisegint  36616  cgrxfr  36643  lineext  36664  btwnconn1lem13  36687  btwnconn1lem14  36688  btwnconn3  36691  brsegle  36696  brsegle2  36697  segleantisym  36703  outsideofeu  36719  lineunray  36735  lineelsb2  36736  cvrcmp  40164  atcvrj2b  40313  3dimlem3  40342  3dimlem3OLDN  40343  3dim3  40350  ps-1  40358  ps-2  40359  lplnnle2at  40422  2llnm3N  40450  4atlem0a  40474  4atlem3  40477  4atlem3a  40478  lnatexN  40660  paddasslem8  40708  paddasslem9  40709  paddasslem10  40710  paddasslem12  40712  paddasslem13  40713  lhpexle2lem  40890  lhpexle3  40893  lhpat3  40927  4atex  40957  trlval2  41044  trlval4  41069  cdleme16  41166  cdleme21  41218  cdleme21k  41219  cdleme27cl  41247  cdleme27N  41250  cdleme43fsv1snlem  41301  cdleme48fvg  41381  cdlemg8  41512  cdlemg15a  41536  cdlemg16z  41540  cdlemg24  41569  cdlemg38  41596  cdlemg40  41598  trlcone  41609  cdlemj2  41703  tendoid0  41706  tendoconid  41710  cdlemk34  41791  cdlemk38  41796  cdlemkid4  41815  cdlemk53  41838  tendospcanN  41904  dihvalcqpre  42116  dihmeetlem15N  42202  qirropth  43757  mzpcong  43821  jm2.26  43851  aomclem6  43908  islptre  46457  limccog  46458  limcleqr  46480  fourierdlem42  46985  elaa2  47070  submodneaddmod  48253  itsclc0b  49710