Theorem simpl23 1253

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

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

This theorem is referenced by:  frrlem10  8231  mulgdirlem  18921  nosupbnd2lem1  27100  noinfbnd2lem1  27115  brbtwn2  27917  ax5seglem3a  27942  ax5seg  27950  axpasch  27953  axeuclid  27975  br8d  31596  br8  34415  cgrextend  34669  segconeq  34671  segconeu  34672  trisegint  34689  ifscgr  34705  cgrsub  34706  cgrxfr  34716  lineext  34737  seglecgr12im  34771  segletr  34775  lineunray  34808  lineelsb2  34809  cvrcmp  37818  cvlsupr2  37878  atcvrj2b  37968  atexchcvrN  37976  3atlem3  38021  3atlem5  38023  lplnnle2at  38077  lplnllnneN  38092  4atlem3  38132  4atlem10b  38141  4atlem12  38148  2llnma3r  38324  paddasslem4  38359  paddasslem7  38362  paddasslem8  38363  paddasslem12  38367  paddasslem13  38368  paddasslem15  38370  pmodlem1  38382  pmodlem2  38383  atmod1i1m  38394  llnexchb2lem  38404  4atex2  38613  ltrnatlw  38719  arglem1N  38726  cdlemd4  38737  cdlemd5  38738  cdleme16  38821  cdleme20  38860  cdleme21k  38874  cdleme27N  38905  cdleme28c  38908  cdleme43fsv1snlem  38956  cdleme38n  39000  cdleme40n  39004  cdleme41snaw  39012  cdlemg6c  39156  cdlemg8c  39165  cdlemg8  39167  cdlemg12e  39183  cdlemg16ALTN  39194  cdlemg16zz  39196  cdlemg18a  39214  cdlemg20  39221  cdlemg22  39223  cdlemg37  39225  cdlemg31d  39236  cdlemg33  39247  cdlemg38  39251  cdlemg44b  39268  cdlemk33N  39445  cdlemk34  39446  cdlemk38  39451  cdlemk35s-id  39474  cdlemk39s-id  39476  cdlemk53b  39492  cdlemk53  39493  cdlemk55  39497  cdlemk35u  39500  cdlemk55u  39502  cdleml3N  39514  cdlemn11pre  39746