Theorem simpl3r 1227

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  tfisi  7680  offsplitfpar  7931  omopth2  8377  ltmul1a  11754  xmulasslem3  12949  xadddi2  12960  swrdsbslen  14305  swrdspsleq  14306  dvdsadd2b  15943  pockthg  16535  psgnunilem4  19020  efgred  19269  marrepeval  21620  submaeval  21639  mdetmul  21680  minmar1eval  21706  ptbasin  22636  basqtop  22770  xrsmopn  23881  axpasch  27212  axeuclid  27234  elwwlks2ons3im  28220  br4  33631  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  btwnouttr2  34251  trisegint  34257  cgrxfr  34284  lineext  34305  btwnconn1lem13  34328  btwnconn1lem14  34329  btwnconn3  34332  brsegle  34337  brsegle2  34338  segleantisym  34344  outsideofeu  34360  lineunray  34376  lineelsb2  34377  cvrcmp  37224  atcvrj2b  37373  3dimlem3  37402  3dimlem3OLDN  37403  3dim3  37410  ps-1  37418  ps-2  37419  lplnnle2at  37482  2llnm3N  37510  4atlem0a  37534  4atlem3  37537  4atlem3a  37538  lnatexN  37720  paddasslem8  37768  paddasslem9  37769  paddasslem10  37770  paddasslem12  37772  paddasslem13  37773  lhpexle2lem  37950  lhpexle3  37953  lhpat3  37987  4atex  38017  trlval2  38104  trlval4  38129  cdleme16  38226  cdleme21  38278  cdleme21k  38279  cdleme27cl  38307  cdleme27N  38310  cdleme43fsv1snlem  38361  cdleme48fvg  38441  cdlemg8  38572  cdlemg15a  38596  cdlemg16z  38600  cdlemg24  38629  cdlemg38  38656  cdlemg40  38658  trlcone  38669  cdlemj2  38763  tendoid0  38766  tendoconid  38770  cdlemk34  38851  cdlemk38  38856  cdlemkid4  38875  cdlemk53  38898  tendospcanN  38964  dihvalcqpre  39176  dihmeetlem15N  39262  qirropth  40646  mzpcong  40710  jm2.26  40740  aomclem6  40800  islptre  43050  limccog  43051  limcleqr  43075  fourierdlem42  43580  elaa2  43665  itsclc0b  46006