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  8231  nosupbnd2lem1  27655  noinfbnd2lem1  27670  brbtwn2  28885  ax5seglem3a  28910  ax5seg  28918  axpasch  28921  axeuclid  28943  br8d  32593  br8  35821  cgrextend  36073  segconeq  36075  trisegint  36093  ifscgr  36109  cgrsub  36110  cgrxfr  36120  lineext  36141  seglecgr12im  36175  segletr  36179  lineunray  36212  lineelsb2  36213  cvrcmp  39402  cvlatexch3  39457  cvlsupr2  39462  atexchcvrN  39559  3dim1  39586  3dim2  39587  ps-1  39596  ps-2  39597  3atlem3  39604  3atlem5  39606  lplnnle2at  39660  lplnllnneN  39675  2llnjaN  39685  4atlem3  39715  4atlem10b  39724  4atlem12  39731  2llnma3r  39907  paddasslem4  39942  paddasslem7  39945  paddasslem8  39946  paddasslem12  39950  paddasslem13  39951  pmodlem1  39965  pmodlem2  39966  llnexchb2lem  39987  4atex2  40196  ltrnatlw  40302  trlval4  40307  arglem1N  40309  cdlemd4  40320  cdlemd5  40321  cdleme0moN  40344  cdleme16  40404  cdleme20  40443  cdleme21j  40455  cdleme21k  40457  cdleme27N  40488  cdleme28c  40491  cdleme43fsv1snlem  40539  cdleme38n  40583  cdleme40n  40587  cdleme41snaw  40595  cdlemg6c  40739  cdlemg8c  40748  cdlemg8  40750  cdlemg12e  40766  cdlemg16  40776  cdlemg16ALTN  40777  cdlemg16z  40778  cdlemg16zz  40779  cdlemg18a  40797  cdlemg20  40804  cdlemg22  40806  cdlemg37  40808  cdlemg27b  40815  cdlemg31d  40819  cdlemg33  40830  cdlemg38  40834  cdlemg44b  40851  cdlemk38  41034  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk55  41080  cdlemk35u  41083  cdlemk55u  41085  cdleml3N  41097  cdlemn11pre  41329