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  7838  offsplitfpar  8101  omopth2  8551  ltmul1a  12038  xmulasslem3  13253  xadddi2  13264  swrdsbslen  14636  swrdspsleq  14637  dvdsadd2b  16283  pockthg  16884  psgnunilem4  19434  efgred  19685  marrepeval  22457  submaeval  22476  mdetmul  22517  minmar1eval  22543  ptbasin  23471  basqtop  23605  xrsmopn  24708  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  precsexlem8  28123  axpasch  28875  axeuclid  28897  elwwlks2ons3im  29891  mhmimasplusg  32986  br4  35752  btwnouttr2  36017  trisegint  36023  cgrxfr  36050  lineext  36071  btwnconn1lem13  36094  btwnconn1lem14  36095  btwnconn3  36098  brsegle  36103  brsegle2  36104  segleantisym  36110  outsideofeu  36126  lineunray  36142  lineelsb2  36143  cvrcmp  39283  atcvrj2b  39433  3dimlem3  39462  3dimlem3OLDN  39463  3dim3  39470  ps-1  39478  ps-2  39479  lplnnle2at  39542  2llnm3N  39570  4atlem0a  39594  4atlem3  39597  4atlem3a  39598  lnatexN  39780  paddasslem8  39828  paddasslem9  39829  paddasslem10  39830  paddasslem12  39832  paddasslem13  39833  lhpexle2lem  40010  lhpexle3  40013  lhpat3  40047  4atex  40077  trlval2  40164  trlval4  40189  cdleme16  40286  cdleme21  40338  cdleme21k  40339  cdleme27cl  40367  cdleme27N  40370  cdleme43fsv1snlem  40421  cdleme48fvg  40501  cdlemg8  40632  cdlemg15a  40656  cdlemg16z  40660  cdlemg24  40689  cdlemg38  40716  cdlemg40  40718  trlcone  40729  cdlemj2  40823  tendoid0  40826  tendoconid  40830  cdlemk34  40911  cdlemk38  40916  cdlemkid4  40935  cdlemk53  40958  tendospcanN  41024  dihvalcqpre  41236  dihmeetlem15N  41322  qirropth  42903  mzpcong  42968  jm2.26  42998  aomclem6  43055  islptre  45624  limccog  45625  limcleqr  45649  fourierdlem42  46154  elaa2  46239  submodneaddmod  47356  itsclc0b  48765