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 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  tfisi  7856  offsplitfpar  8115  omopth2  8570  ltmul1a  12065  xmulasslem3  13313  xadddi2  13324  swrdsbslen  14704  swrdspsleq  14705  dvdsadd2b  16365  pockthg  16967  psgnunilem4  19568  efgred  19819  marrepeval  22701  submaeval  22720  mdetmul  22761  minmar1eval  22787  ptbasin  23715  basqtop  23849  xrsmopn  24951  nosupbnd1lem3  27852  nosupbnd1lem4  27853  nosupbnd1lem5  27854  noinfbnd1lem3  27867  noinfbnd1lem4  27868  noinfbnd1lem5  27869  precsexlem8  28385  axpasch  29269  axeuclid  29291  elwwlks2ons3im  30281  mhmimasplusg  33335  br4  36228  btwnouttr2  36492  trisegint  36498  cgrxfr  36525  lineext  36546  btwnconn1lem13  36569  btwnconn1lem14  36570  btwnconn3  36573  brsegle  36578  brsegle2  36579  segleantisym  36585  outsideofeu  36601  lineunray  36617  lineelsb2  36618  cvrcmp  40035  atcvrj2b  40184  3dimlem3  40213  3dimlem3OLDN  40214  3dim3  40221  ps-1  40229  ps-2  40230  lplnnle2at  40293  2llnm3N  40321  4atlem0a  40345  4atlem3  40348  4atlem3a  40349  lnatexN  40531  paddasslem8  40579  paddasslem9  40580  paddasslem10  40581  paddasslem12  40583  paddasslem13  40584  lhpexle2lem  40761  lhpexle3  40764  lhpat3  40798  4atex  40828  trlval2  40915  trlval4  40940  cdleme16  41037  cdleme21  41089  cdleme21k  41090  cdleme27cl  41118  cdleme27N  41121  cdleme43fsv1snlem  41172  cdleme48fvg  41252  cdlemg8  41383  cdlemg15a  41407  cdlemg16z  41411  cdlemg24  41440  cdlemg38  41467  cdlemg40  41469  trlcone  41480  cdlemj2  41574  tendoid0  41577  tendoconid  41581  cdlemk34  41662  cdlemk38  41667  cdlemkid4  41686  cdlemk53  41709  tendospcanN  41775  dihvalcqpre  41987  dihmeetlem15N  42073  qirropth  43615  mzpcong  43679  jm2.26  43709  aomclem6  43766  islptre  46315  limccog  46316  limcleqr  46338  fourierdlem42  46843  elaa2  46928  submodneaddmod  48071  itsclc0b  49529