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

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

This theorem is referenced by:  tfisi  7879  offsplitfpar  8142  omopth2  8620  ltmul1a  12113  xmulasslem3  13324  xadddi2  13335  swrdsbslen  14698  swrdspsleq  14699  dvdsadd2b  16339  pockthg  16939  psgnunilem4  19529  efgred  19780  marrepeval  22584  submaeval  22603  mdetmul  22644  minmar1eval  22670  ptbasin  23600  basqtop  23734  xrsmopn  24847  nosupbnd1lem3  27769  nosupbnd1lem4  27770  nosupbnd1lem5  27771  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  precsexlem8  28252  axpasch  28970  axeuclid  28992  elwwlks2ons3im  29983  mhmimasplusg  33025  br4  35737  btwnouttr2  36003  trisegint  36009  cgrxfr  36036  lineext  36057  btwnconn1lem13  36080  btwnconn1lem14  36081  btwnconn3  36084  brsegle  36089  brsegle2  36090  segleantisym  36096  outsideofeu  36112  lineunray  36128  lineelsb2  36129  cvrcmp  39264  atcvrj2b  39414  3dimlem3  39443  3dimlem3OLDN  39444  3dim3  39451  ps-1  39459  ps-2  39460  lplnnle2at  39523  2llnm3N  39551  4atlem0a  39575  4atlem3  39578  4atlem3a  39579  lnatexN  39761  paddasslem8  39809  paddasslem9  39810  paddasslem10  39811  paddasslem12  39813  paddasslem13  39814  lhpexle2lem  39991  lhpexle3  39994  lhpat3  40028  4atex  40058  trlval2  40145  trlval4  40170  cdleme16  40267  cdleme21  40319  cdleme21k  40320  cdleme27cl  40348  cdleme27N  40351  cdleme43fsv1snlem  40402  cdleme48fvg  40482  cdlemg8  40613  cdlemg15a  40637  cdlemg16z  40641  cdlemg24  40670  cdlemg38  40697  cdlemg40  40699  trlcone  40710  cdlemj2  40804  tendoid0  40807  tendoconid  40811  cdlemk34  40892  cdlemk38  40897  cdlemkid4  40916  cdlemk53  40939  tendospcanN  41005  dihvalcqpre  41217  dihmeetlem15N  41303  qirropth  42895  mzpcong  42960  jm2.26  42990  aomclem6  43047  islptre  45574  limccog  45575  limcleqr  45599  fourierdlem42  46104  elaa2  46189  submodneaddmod  47290  itsclc0b  48621