Theorem simpl23 1255

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 1195	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1188	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:  frrlem10  8247  mulgdirlem  19047  nosupbnd2lem1  27695  noinfbnd2lem1  27710  brbtwn2  28990  ax5seglem3a  29015  ax5seg  29023  axpasch  29026  axeuclid  29048  br8d  32697  br8  35969  cgrextend  36221  segconeq  36223  segconeu  36224  trisegint  36241  ifscgr  36257  cgrsub  36258  cgrxfr  36268  lineext  36289  seglecgr12im  36323  segletr  36327  lineunray  36360  lineelsb2  36361  cvrcmp  39653  cvlsupr2  39713  atcvrj2b  39802  atexchcvrN  39810  3atlem3  39855  3atlem5  39857  lplnnle2at  39911  lplnllnneN  39926  4atlem3  39966  4atlem10b  39975  4atlem12  39982  2llnma3r  40158  paddasslem4  40193  paddasslem7  40196  paddasslem8  40197  paddasslem12  40201  paddasslem13  40202  paddasslem15  40204  pmodlem1  40216  pmodlem2  40217  atmod1i1m  40228  llnexchb2lem  40238  4atex2  40447  ltrnatlw  40553  arglem1N  40560  cdlemd4  40571  cdlemd5  40572  cdleme16  40655  cdleme20  40694  cdleme21k  40708  cdleme27N  40739  cdleme28c  40742  cdleme43fsv1snlem  40790  cdleme38n  40834  cdleme40n  40838  cdleme41snaw  40846  cdlemg6c  40990  cdlemg8c  40999  cdlemg8  41001  cdlemg12e  41017  cdlemg16ALTN  41028  cdlemg16zz  41030  cdlemg18a  41048  cdlemg20  41055  cdlemg22  41057  cdlemg37  41059  cdlemg31d  41070  cdlemg33  41081  cdlemg38  41085  cdlemg44b  41102  cdlemk33N  41279  cdlemk34  41280  cdlemk38  41285  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk53b  41326  cdlemk53  41327  cdlemk55  41331  cdlemk35u  41334  cdlemk55u  41336  cdleml3N  41348  cdlemn11pre  41580  aks6d1c1  42480