Theorem simpl3r 1231

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 1189	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  tfisi  7637  offsplitfpar  7888  omopth2  8312  ltmul1a  11681  xmulasslem3  12876  xadddi2  12887  swrdsbslen  14229  swrdspsleq  14230  dvdsadd2b  15867  pockthg  16459  psgnunilem4  18889  efgred  19138  marrepeval  21460  submaeval  21479  mdetmul  21520  minmar1eval  21546  ptbasin  22474  basqtop  22608  xrsmopn  23709  axpasch  27032  axeuclid  27054  elwwlks2ons3im  28038  br4  33444  nosupbnd1lem3  33650  nosupbnd1lem4  33651  nosupbnd1lem5  33652  noinfbnd1lem3  33665  noinfbnd1lem4  33666  noinfbnd1lem5  33667  btwnouttr2  34061  trisegint  34067  cgrxfr  34094  lineext  34115  btwnconn1lem13  34138  btwnconn1lem14  34139  btwnconn3  34142  brsegle  34147  brsegle2  34148  segleantisym  34154  outsideofeu  34170  lineunray  34186  lineelsb2  34187  cvrcmp  37034  atcvrj2b  37183  3dimlem3  37212  3dimlem3OLDN  37213  3dim3  37220  ps-1  37228  ps-2  37229  lplnnle2at  37292  2llnm3N  37320  4atlem0a  37344  4atlem3  37347  4atlem3a  37348  lnatexN  37530  paddasslem8  37578  paddasslem9  37579  paddasslem10  37580  paddasslem12  37582  paddasslem13  37583  lhpexle2lem  37760  lhpexle3  37763  lhpat3  37797  4atex  37827  trlval2  37914  trlval4  37939  cdleme16  38036  cdleme21  38088  cdleme21k  38089  cdleme27cl  38117  cdleme27N  38120  cdleme43fsv1snlem  38171  cdleme48fvg  38251  cdlemg8  38382  cdlemg15a  38406  cdlemg16z  38410  cdlemg24  38439  cdlemg38  38466  cdlemg40  38468  trlcone  38479  cdlemj2  38573  tendoid0  38576  tendoconid  38580  cdlemk34  38661  cdlemk38  38666  cdlemkid4  38685  cdlemk53  38708  tendospcanN  38774  dihvalcqpre  38986  dihmeetlem15N  39072  qirropth  40433  mzpcong  40497  jm2.26  40527  aomclem6  40587  islptre  42835  limccog  42836  limcleqr  42860  fourierdlem42  43365  elaa2  43450  itsclc0b  45791