Theorem simpl23 1233

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl23	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Proof of Theorem simpl23

Step	Hyp	Ref	Expression
1		simpl3 1173	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1166	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  mulgdirlem  18045  brbtwn2  26397  ax5seglem3a  26422  ax5seg  26430  axpasch  26433  axeuclid  26455  br8d  30128  br8  32512  frrlem10  32653  nosupbnd2lem1  32736  cgrextend  32990  segconeq  32992  segconeu  32993  trisegint  33010  ifscgr  33026  cgrsub  33027  cgrxfr  33037  lineext  33058  seglecgr12im  33092  segletr  33096  lineunray  33129  lineelsb2  33130  cvrcmp  35864  cvlsupr2  35924  atcvrj2b  36013  atexchcvrN  36021  3atlem3  36066  3atlem5  36068  lplnnle2at  36122  lplnllnneN  36137  4atlem3  36177  4atlem10b  36186  4atlem12  36193  2llnma3r  36369  paddasslem4  36404  paddasslem7  36407  paddasslem8  36408  paddasslem12  36412  paddasslem13  36413  paddasslem15  36415  pmodlem1  36427  pmodlem2  36428  atmod1i1m  36439  llnexchb2lem  36449  4atex2  36658  ltrnatlw  36764  arglem1N  36771  cdlemd4  36782  cdlemd5  36783  cdleme16  36866  cdleme20  36905  cdleme21k  36919  cdleme27N  36950  cdleme28c  36953  cdleme43fsv1snlem  37001  cdleme38n  37045  cdleme40n  37049  cdleme41snaw  37057  cdlemg6c  37201  cdlemg8c  37210  cdlemg8  37212  cdlemg12e  37228  cdlemg16ALTN  37239  cdlemg16zz  37241  cdlemg18a  37259  cdlemg20  37266  cdlemg22  37268  cdlemg37  37270  cdlemg31d  37281  cdlemg33  37292  cdlemg38  37296  cdlemg44b  37313  cdlemk33N  37490  cdlemk34  37491  cdlemk38  37496  cdlemk35s-id  37519  cdlemk39s-id  37521  cdlemk53b  37537  cdlemk53  37538  cdlemk55  37542  cdlemk35u  37545  cdlemk55u  37547  cdleml3N  37559  cdlemn11pre  37791