Theorem simpl3r 1230

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfisi  7854  offsplitfpar  8118  omopth2  8596  ltmul1a  12090  xmulasslem3  13302  xadddi2  13313  swrdsbslen  14682  swrdspsleq  14683  dvdsadd2b  16325  pockthg  16926  psgnunilem4  19478  efgred  19729  marrepeval  22501  submaeval  22520  mdetmul  22561  minmar1eval  22587  ptbasin  23515  basqtop  23649  xrsmopn  24752  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  precsexlem8  28168  axpasch  28920  axeuclid  28942  elwwlks2ons3im  29936  mhmimasplusg  33033  br4  35775  btwnouttr2  36040  trisegint  36046  cgrxfr  36073  lineext  36094  btwnconn1lem13  36117  btwnconn1lem14  36118  btwnconn3  36121  brsegle  36126  brsegle2  36127  segleantisym  36133  outsideofeu  36149  lineunray  36165  lineelsb2  36166  cvrcmp  39301  atcvrj2b  39451  3dimlem3  39480  3dimlem3OLDN  39481  3dim3  39488  ps-1  39496  ps-2  39497  lplnnle2at  39560  2llnm3N  39588  4atlem0a  39612  4atlem3  39615  4atlem3a  39616  lnatexN  39798  paddasslem8  39846  paddasslem9  39847  paddasslem10  39848  paddasslem12  39850  paddasslem13  39851  lhpexle2lem  40028  lhpexle3  40031  lhpat3  40065  4atex  40095  trlval2  40182  trlval4  40207  cdleme16  40304  cdleme21  40356  cdleme21k  40357  cdleme27cl  40385  cdleme27N  40388  cdleme43fsv1snlem  40439  cdleme48fvg  40519  cdlemg8  40650  cdlemg15a  40674  cdlemg16z  40678  cdlemg24  40707  cdlemg38  40734  cdlemg40  40736  trlcone  40747  cdlemj2  40841  tendoid0  40844  tendoconid  40848  cdlemk34  40929  cdlemk38  40934  cdlemkid4  40953  cdlemk53  40976  tendospcanN  41042  dihvalcqpre  41254  dihmeetlem15N  41340  qirropth  42931  mzpcong  42996  jm2.26  43026  aomclem6  43083  islptre  45648  limccog  45649  limcleqr  45673  fourierdlem42  46178  elaa2  46263  submodneaddmod  47380  itsclc0b  48752