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  7799  offsplitfpar  8059  omopth2  8509  ltmul1a  11991  xmulasslem3  13206  xadddi2  13217  swrdsbslen  14589  swrdspsleq  14590  dvdsadd2b  16235  pockthg  16836  psgnunilem4  19394  efgred  19645  marrepeval  22466  submaeval  22485  mdetmul  22526  minmar1eval  22552  ptbasin  23480  basqtop  23614  xrsmopn  24717  nosupbnd1lem3  27638  nosupbnd1lem4  27639  nosupbnd1lem5  27640  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  precsexlem8  28139  axpasch  28904  axeuclid  28926  elwwlks2ons3im  29917  mhmimasplusg  33005  br4  35730  btwnouttr2  35995  trisegint  36001  cgrxfr  36028  lineext  36049  btwnconn1lem13  36072  btwnconn1lem14  36073  btwnconn3  36076  brsegle  36081  brsegle2  36082  segleantisym  36088  outsideofeu  36104  lineunray  36120  lineelsb2  36121  cvrcmp  39261  atcvrj2b  39411  3dimlem3  39440  3dimlem3OLDN  39441  3dim3  39448  ps-1  39456  ps-2  39457  lplnnle2at  39520  2llnm3N  39548  4atlem0a  39572  4atlem3  39575  4atlem3a  39576  lnatexN  39758  paddasslem8  39806  paddasslem9  39807  paddasslem10  39808  paddasslem12  39810  paddasslem13  39811  lhpexle2lem  39988  lhpexle3  39991  lhpat3  40025  4atex  40055  trlval2  40142  trlval4  40167  cdleme16  40264  cdleme21  40316  cdleme21k  40317  cdleme27cl  40345  cdleme27N  40348  cdleme43fsv1snlem  40399  cdleme48fvg  40479  cdlemg8  40610  cdlemg15a  40634  cdlemg16z  40638  cdlemg24  40667  cdlemg38  40694  cdlemg40  40696  trlcone  40707  cdlemj2  40801  tendoid0  40804  tendoconid  40808  cdlemk34  40889  cdlemk38  40894  cdlemkid4  40913  cdlemk53  40936  tendospcanN  41002  dihvalcqpre  41214  dihmeetlem15N  41300  qirropth  42881  mzpcong  42945  jm2.26  42975  aomclem6  43032  islptre  45601  limccog  45602  limcleqr  45626  fourierdlem42  46131  elaa2  46216  submodneaddmod  47336  itsclc0b  48758