Theorem simpl21 1253

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

Assertion

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

Proof of Theorem simpl21

Step	Hyp	Ref	Expression
1		simpl1 1193	. 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  nosupbnd2lem1  27695  noinfbnd2lem1  27710  brbtwn2  28990  ax5seglem3a  29015  ax5seg  29023  axpasch  29026  axeuclid  29048  br8d  32697  br8  35969  cgrextend  36221  segconeq  36223  trisegint  36241  ifscgr  36257  cgrsub  36258  cgrxfr  36268  lineext  36289  seglecgr12im  36323  segletr  36327  lineunray  36360  lineelsb2  36361  cvrcmp  39653  cvlatexch3  39708  cvlsupr2  39713  atexchcvrN  39810  3dim1  39837  3dim2  39838  ps-1  39847  ps-2  39848  3atlem3  39855  3atlem5  39857  lplnnle2at  39911  lplnllnneN  39926  2llnjaN  39936  4atlem3  39966  4atlem10b  39975  4atlem12  39982  2llnma3r  40158  paddasslem4  40193  paddasslem7  40196  paddasslem8  40197  paddasslem12  40201  paddasslem13  40202  pmodlem1  40216  pmodlem2  40217  llnexchb2lem  40238  4atex2  40447  ltrnatlw  40553  trlval4  40558  arglem1N  40560  cdlemd4  40571  cdlemd5  40572  cdleme0moN  40595  cdleme16  40655  cdleme20  40694  cdleme21j  40706  cdleme21k  40708  cdleme27N  40739  cdleme28c  40742  cdleme43fsv1snlem  40790  cdleme38n  40834  cdleme40n  40838  cdleme41snaw  40846  cdlemg6c  40990  cdlemg8c  40999  cdlemg8  41001  cdlemg12e  41017  cdlemg16  41027  cdlemg16ALTN  41028  cdlemg16z  41029  cdlemg16zz  41030  cdlemg18a  41048  cdlemg20  41055  cdlemg22  41057  cdlemg37  41059  cdlemg27b  41066  cdlemg31d  41070  cdlemg33  41081  cdlemg38  41085  cdlemg44b  41102  cdlemk38  41285  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk55  41331  cdlemk35u  41334  cdlemk55u  41336  cdleml3N  41348  cdlemn11pre  41580