Theorem simpl3r 1229

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 1187	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  7896  offsplitfpar  8160  omopth2  8640  ltmul1a  12143  xmulasslem3  13348  xadddi2  13359  swrdsbslen  14712  swrdspsleq  14713  dvdsadd2b  16354  pockthg  16953  psgnunilem4  19539  efgred  19790  marrepeval  22590  submaeval  22609  mdetmul  22650  minmar1eval  22676  ptbasin  23606  basqtop  23740  xrsmopn  24853  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  precsexlem8  28256  axpasch  28974  axeuclid  28996  elwwlks2ons3im  29987  mhmimasplusg  33024  br4  35720  btwnouttr2  35986  trisegint  35992  cgrxfr  36019  lineext  36040  btwnconn1lem13  36063  btwnconn1lem14  36064  btwnconn3  36067  brsegle  36072  brsegle2  36073  segleantisym  36079  outsideofeu  36095  lineunray  36111  lineelsb2  36112  cvrcmp  39239  atcvrj2b  39389  3dimlem3  39418  3dimlem3OLDN  39419  3dim3  39426  ps-1  39434  ps-2  39435  lplnnle2at  39498  2llnm3N  39526  4atlem0a  39550  4atlem3  39553  4atlem3a  39554  lnatexN  39736  paddasslem8  39784  paddasslem9  39785  paddasslem10  39786  paddasslem12  39788  paddasslem13  39789  lhpexle2lem  39966  lhpexle3  39969  lhpat3  40003  4atex  40033  trlval2  40120  trlval4  40145  cdleme16  40242  cdleme21  40294  cdleme21k  40295  cdleme27cl  40323  cdleme27N  40326  cdleme43fsv1snlem  40377  cdleme48fvg  40457  cdlemg8  40588  cdlemg15a  40612  cdlemg16z  40616  cdlemg24  40645  cdlemg38  40672  cdlemg40  40674  trlcone  40685  cdlemj2  40779  tendoid0  40782  tendoconid  40786  cdlemk34  40867  cdlemk38  40872  cdlemkid4  40891  cdlemk53  40914  tendospcanN  40980  dihvalcqpre  41192  dihmeetlem15N  41278  qirropth  42864  mzpcong  42929  jm2.26  42959  aomclem6  43016  islptre  45540  limccog  45541  limcleqr  45565  fourierdlem42  46070  elaa2  46155  itsclc0b  48506