Theorem simpl3r 1231

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

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

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 1089

This theorem is referenced by:  tfisi  7803  offsplitfpar  8062  omopth2  8512  ltmul1a  11995  xmulasslem3  13229  xadddi2  13240  swrdsbslen  14618  swrdspsleq  14619  dvdsadd2b  16266  pockthg  16868  psgnunilem4  19463  efgred  19714  marrepeval  22538  submaeval  22557  mdetmul  22598  minmar1eval  22624  ptbasin  23552  basqtop  23686  xrsmopn  24788  nosupbnd1lem3  27688  nosupbnd1lem4  27689  nosupbnd1lem5  27690  noinfbnd1lem3  27703  noinfbnd1lem4  27704  noinfbnd1lem5  27705  precsexlem8  28220  axpasch  29024  axeuclid  29046  elwwlks2ons3im  30037  mhmimasplusg  33113  br4  35956  btwnouttr2  36220  trisegint  36226  cgrxfr  36253  lineext  36274  btwnconn1lem13  36297  btwnconn1lem14  36298  btwnconn3  36301  brsegle  36306  brsegle2  36307  segleantisym  36313  outsideofeu  36329  lineunray  36345  lineelsb2  36346  cvrcmp  39743  atcvrj2b  39892  3dimlem3  39921  3dimlem3OLDN  39922  3dim3  39929  ps-1  39937  ps-2  39938  lplnnle2at  40001  2llnm3N  40029  4atlem0a  40053  4atlem3  40056  4atlem3a  40057  lnatexN  40239  paddasslem8  40287  paddasslem9  40288  paddasslem10  40289  paddasslem12  40291  paddasslem13  40292  lhpexle2lem  40469  lhpexle3  40472  lhpat3  40506  4atex  40536  trlval2  40623  trlval4  40648  cdleme16  40745  cdleme21  40797  cdleme21k  40798  cdleme27cl  40826  cdleme27N  40829  cdleme43fsv1snlem  40880  cdleme48fvg  40960  cdlemg8  41091  cdlemg15a  41115  cdlemg16z  41119  cdlemg24  41148  cdlemg38  41175  cdlemg40  41177  trlcone  41188  cdlemj2  41282  tendoid0  41285  tendoconid  41289  cdlemk34  41370  cdlemk38  41375  cdlemkid4  41394  cdlemk53  41417  tendospcanN  41483  dihvalcqpre  41695  dihmeetlem15N  41781  qirropth  43354  mzpcong  43418  jm2.26  43448  aomclem6  43505  islptre  46067  limccog  46068  limcleqr  46090  fourierdlem42  46595  elaa2  46680  submodneaddmod  47817  itsclc0b  49260