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

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

This theorem is referenced by:  tfisi  7778  offsplitfpar  8032  omopth2  8491  ltmul1a  11930  xmulasslem3  13126  xadddi2  13137  swrdsbslen  14476  swrdspsleq  14477  dvdsadd2b  16115  pockthg  16705  psgnunilem4  19202  efgred  19450  marrepeval  21818  submaeval  21837  mdetmul  21878  minmar1eval  21904  ptbasin  22834  basqtop  22968  xrsmopn  24081  nosupbnd1lem3  26964  nosupbnd1lem4  26965  nosupbnd1lem5  26966  noinfbnd1lem3  26979  noinfbnd1lem4  26980  noinfbnd1lem5  26981  axpasch  27598  axeuclid  27620  elwwlks2ons3im  28607  br4  34014  btwnouttr2  34461  trisegint  34467  cgrxfr  34494  lineext  34515  btwnconn1lem13  34538  btwnconn1lem14  34539  btwnconn3  34542  brsegle  34547  brsegle2  34548  segleantisym  34554  outsideofeu  34570  lineunray  34586  lineelsb2  34587  cvrcmp  37599  atcvrj2b  37749  3dimlem3  37778  3dimlem3OLDN  37779  3dim3  37786  ps-1  37794  ps-2  37795  lplnnle2at  37858  2llnm3N  37886  4atlem0a  37910  4atlem3  37913  4atlem3a  37914  lnatexN  38096  paddasslem8  38144  paddasslem9  38145  paddasslem10  38146  paddasslem12  38148  paddasslem13  38149  lhpexle2lem  38326  lhpexle3  38329  lhpat3  38363  4atex  38393  trlval2  38480  trlval4  38505  cdleme16  38602  cdleme21  38654  cdleme21k  38655  cdleme27cl  38683  cdleme27N  38686  cdleme43fsv1snlem  38737  cdleme48fvg  38817  cdlemg8  38948  cdlemg15a  38972  cdlemg16z  38976  cdlemg24  39005  cdlemg38  39032  cdlemg40  39034  trlcone  39045  cdlemj2  39139  tendoid0  39142  tendoconid  39146  cdlemk34  39227  cdlemk38  39232  cdlemkid4  39251  cdlemk53  39274  tendospcanN  39340  dihvalcqpre  39552  dihmeetlem15N  39638  qirropth  41041  mzpcong  41106  jm2.26  41136  aomclem6  41196  islptre  43546  limccog  43547  limcleqr  43571  fourierdlem42  44076  elaa2  44161  itsclc0b  46534