Theorem simpl3r 1228

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  tfisi  7714  offsplitfpar  7969  omopth2  8424  ltmul1a  11833  xmulasslem3  13029  xadddi2  13040  swrdsbslen  14386  swrdspsleq  14387  dvdsadd2b  16024  pockthg  16616  psgnunilem4  19114  efgred  19363  marrepeval  21721  submaeval  21740  mdetmul  21781  minmar1eval  21807  ptbasin  22737  basqtop  22871  xrsmopn  23984  axpasch  27318  axeuclid  27340  elwwlks2ons3im  28328  br4  33734  nosupbnd1lem3  33922  nosupbnd1lem4  33923  nosupbnd1lem5  33924  noinfbnd1lem3  33937  noinfbnd1lem4  33938  noinfbnd1lem5  33939  btwnouttr2  34333  trisegint  34339  cgrxfr  34366  lineext  34387  btwnconn1lem13  34410  btwnconn1lem14  34411  btwnconn3  34414  brsegle  34419  brsegle2  34420  segleantisym  34426  outsideofeu  34442  lineunray  34458  lineelsb2  34459  cvrcmp  37304  atcvrj2b  37453  3dimlem3  37482  3dimlem3OLDN  37483  3dim3  37490  ps-1  37498  ps-2  37499  lplnnle2at  37562  2llnm3N  37590  4atlem0a  37614  4atlem3  37617  4atlem3a  37618  lnatexN  37800  paddasslem8  37848  paddasslem9  37849  paddasslem10  37850  paddasslem12  37852  paddasslem13  37853  lhpexle2lem  38030  lhpexle3  38033  lhpat3  38067  4atex  38097  trlval2  38184  trlval4  38209  cdleme16  38306  cdleme21  38358  cdleme21k  38359  cdleme27cl  38387  cdleme27N  38390  cdleme43fsv1snlem  38441  cdleme48fvg  38521  cdlemg8  38652  cdlemg15a  38676  cdlemg16z  38680  cdlemg24  38709  cdlemg38  38736  cdlemg40  38738  trlcone  38749  cdlemj2  38843  tendoid0  38846  tendoconid  38850  cdlemk34  38931  cdlemk38  38936  cdlemkid4  38955  cdlemk53  38978  tendospcanN  39044  dihvalcqpre  39256  dihmeetlem15N  39342  qirropth  40737  mzpcong  40801  jm2.26  40831  aomclem6  40891  islptre  43167  limccog  43168  limcleqr  43192  fourierdlem42  43697  elaa2  43782  itsclc0b  46129