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  7894  offsplitfpar  8157  omopth2  8620  ltmul1a  12193  xmulasslem3  13443  xadddi2  13454  swrdsbslen  14842  swrdspsleq  14843  dvdsadd2b  16505  pockthg  17113  psgnunilem4  19741  efgred  19992  marrepeval  22908  submaeval  22927  mdetmul  22968  minmar1eval  22994  ptbasin  23926  basqtop  24060  xrsmopn  25162  nosupbnd1lem3  28097  nosupbnd1lem4  28098  nosupbnd1lem5  28099  noinfbnd1lem3  28112  noinfbnd1lem4  28113  noinfbnd1lem5  28114  precsexlem8  28630  axpasch  29549  axeuclid  29571  elwwlks2ons3im  30573  mhmimasplusg  33668  br4  36701  btwnouttr2  36965  trisegint  36971  cgrxfr  36998  lineext  37019  btwnconn1lem13  37042  btwnconn1lem14  37043  btwnconn3  37046  brsegle  37051  brsegle2  37052  segleantisym  37058  outsideofeu  37074  lineunray  37090  lineelsb2  37091  cvrcmp  40532  atcvrj2b  40681  3dimlem3  40710  3dimlem3OLDN  40711  3dim3  40718  ps-1  40726  ps-2  40727  lplnnle2at  40790  2llnm3N  40818  4atlem0a  40842  4atlem3  40845  4atlem3a  40846  lnatexN  41028  paddasslem8  41076  paddasslem9  41077  paddasslem10  41078  paddasslem12  41080  paddasslem13  41081  lhpexle2lem  41258  lhpexle3  41261  lhpat3  41295  4atex  41325  trlval2  41412  trlval4  41437  cdleme16  41534  cdleme21  41586  cdleme21k  41587  cdleme27cl  41615  cdleme27N  41618  cdleme43fsv1snlem  41669  cdleme48fvg  41749  cdlemg8  41880  cdlemg15a  41904  cdlemg16z  41908  cdlemg24  41937  cdlemg38  41964  cdlemg40  41966  trlcone  41977  cdlemj2  42071  tendoid0  42074  tendoconid  42078  cdlemk34  42159  cdlemk38  42164  cdlemkid4  42183  cdlemk53  42206  tendospcanN  42272  dihvalcqpre  42484  dihmeetlem15N  42570  qirropth  44108  mzpcong  44172  jm2.26  44202  aomclem6  44254  islptre  46836  limccog  46837  limcleqr  46859  fourierdlem42  47364  elaa2  47449  submodneaddmod  48632  itsclc0b  50089