Theorem simpl21 1252

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  frrlem10  8237  nosupbnd2lem1  27683  noinfbnd2lem1  27698  brbtwn2  28978  ax5seglem3a  29003  ax5seg  29011  axpasch  29014  axeuclid  29036  br8d  32686  br8  35950  cgrextend  36202  segconeq  36204  trisegint  36222  ifscgr  36238  cgrsub  36239  cgrxfr  36249  lineext  36270  seglecgr12im  36304  segletr  36308  lineunray  36341  lineelsb2  36342  cvrcmp  39539  cvlatexch3  39594  cvlsupr2  39599  atexchcvrN  39696  3dim1  39723  3dim2  39724  ps-1  39733  ps-2  39734  3atlem3  39741  3atlem5  39743  lplnnle2at  39797  lplnllnneN  39812  2llnjaN  39822  4atlem3  39852  4atlem10b  39861  4atlem12  39868  2llnma3r  40044  paddasslem4  40079  paddasslem7  40082  paddasslem8  40083  paddasslem12  40087  paddasslem13  40088  pmodlem1  40102  pmodlem2  40103  llnexchb2lem  40124  4atex2  40333  ltrnatlw  40439  trlval4  40444  arglem1N  40446  cdlemd4  40457  cdlemd5  40458  cdleme0moN  40481  cdleme16  40541  cdleme20  40580  cdleme21j  40592  cdleme21k  40594  cdleme27N  40625  cdleme28c  40628  cdleme43fsv1snlem  40676  cdleme38n  40720  cdleme40n  40724  cdleme41snaw  40732  cdlemg6c  40876  cdlemg8c  40885  cdlemg8  40887  cdlemg12e  40903  cdlemg16  40913  cdlemg16ALTN  40914  cdlemg16z  40915  cdlemg16zz  40916  cdlemg18a  40934  cdlemg20  40941  cdlemg22  40943  cdlemg37  40945  cdlemg27b  40952  cdlemg31d  40956  cdlemg33  40967  cdlemg38  40971  cdlemg44b  40988  cdlemk38  41171  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk55  41217  cdlemk35u  41220  cdlemk55u  41222  cdleml3N  41234  cdlemn11pre  41466