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 769	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl3 1188	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  7880  offsplitfpar  8144  omopth2  8622  ltmul1a  12116  xmulasslem3  13328  xadddi2  13339  swrdsbslen  14702  swrdspsleq  14703  dvdsadd2b  16343  pockthg  16944  psgnunilem4  19515  efgred  19766  marrepeval  22569  submaeval  22588  mdetmul  22629  minmar1eval  22655  ptbasin  23585  basqtop  23719  xrsmopn  24834  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  precsexlem8  28238  axpasch  28956  axeuclid  28978  elwwlks2ons3im  29974  mhmimasplusg  33043  br4  35758  btwnouttr2  36023  trisegint  36029  cgrxfr  36056  lineext  36077  btwnconn1lem13  36100  btwnconn1lem14  36101  btwnconn3  36104  brsegle  36109  brsegle2  36110  segleantisym  36116  outsideofeu  36132  lineunray  36148  lineelsb2  36149  cvrcmp  39284  atcvrj2b  39434  3dimlem3  39463  3dimlem3OLDN  39464  3dim3  39471  ps-1  39479  ps-2  39480  lplnnle2at  39543  2llnm3N  39571  4atlem0a  39595  4atlem3  39598  4atlem3a  39599  lnatexN  39781  paddasslem8  39829  paddasslem9  39830  paddasslem10  39831  paddasslem12  39833  paddasslem13  39834  lhpexle2lem  40011  lhpexle3  40014  lhpat3  40048  4atex  40078  trlval2  40165  trlval4  40190  cdleme16  40287  cdleme21  40339  cdleme21k  40340  cdleme27cl  40368  cdleme27N  40371  cdleme43fsv1snlem  40422  cdleme48fvg  40502  cdlemg8  40633  cdlemg15a  40657  cdlemg16z  40661  cdlemg24  40690  cdlemg38  40717  cdlemg40  40719  trlcone  40730  cdlemj2  40824  tendoid0  40827  tendoconid  40831  cdlemk34  40912  cdlemk38  40917  cdlemkid4  40936  cdlemk53  40959  tendospcanN  41025  dihvalcqpre  41237  dihmeetlem15N  41323  qirropth  42919  mzpcong  42984  jm2.26  43014  aomclem6  43071  islptre  45634  limccog  45635  limcleqr  45659  fourierdlem42  46164  elaa2  46249  submodneaddmod  47353  itsclc0b  48693