Theorem simpl23 1249

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 1189	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1182	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  mulgdirlem  18258  brbtwn2  26691  ax5seglem3a  26716  ax5seg  26724  axpasch  26727  axeuclid  26749  br8d  30361  br8  32992  frrlem10  33132  nosupbnd2lem1  33215  cgrextend  33469  segconeq  33471  segconeu  33472  trisegint  33489  ifscgr  33505  cgrsub  33506  cgrxfr  33516  lineext  33537  seglecgr12im  33571  segletr  33575  lineunray  33608  lineelsb2  33609  cvrcmp  36434  cvlsupr2  36494  atcvrj2b  36583  atexchcvrN  36591  3atlem3  36636  3atlem5  36638  lplnnle2at  36692  lplnllnneN  36707  4atlem3  36747  4atlem10b  36756  4atlem12  36763  2llnma3r  36939  paddasslem4  36974  paddasslem7  36977  paddasslem8  36978  paddasslem12  36982  paddasslem13  36983  paddasslem15  36985  pmodlem1  36997  pmodlem2  36998  atmod1i1m  37009  llnexchb2lem  37019  4atex2  37228  ltrnatlw  37334  arglem1N  37341  cdlemd4  37352  cdlemd5  37353  cdleme16  37436  cdleme20  37475  cdleme21k  37489  cdleme27N  37520  cdleme28c  37523  cdleme43fsv1snlem  37571  cdleme38n  37615  cdleme40n  37619  cdleme41snaw  37627  cdlemg6c  37771  cdlemg8c  37780  cdlemg8  37782  cdlemg12e  37798  cdlemg16ALTN  37809  cdlemg16zz  37811  cdlemg18a  37829  cdlemg20  37836  cdlemg22  37838  cdlemg37  37840  cdlemg31d  37851  cdlemg33  37862  cdlemg38  37866  cdlemg44b  37883  cdlemk33N  38060  cdlemk34  38061  cdlemk38  38066  cdlemk35s-id  38089  cdlemk39s-id  38091  cdlemk53b  38107  cdlemk53  38108  cdlemk55  38112  cdlemk35u  38115  cdlemk55u  38117  cdleml3N  38129  cdlemn11pre  38361