Theorem simpl21 1242

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1078

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 208  df-an 397  df-3an 1080

This theorem is referenced by:  brbtwn2  26362  ax5seglem3a  26387  ax5seg  26395  axpasch  26398  axeuclid  26420  br8d  30026  br8  32545  frrlem10  32686  nosupbnd2lem1  32769  cgrextend  33023  segconeq  33025  trisegint  33043  ifscgr  33059  cgrsub  33060  cgrxfr  33070  lineext  33091  seglecgr12im  33125  segletr  33129  lineunray  33162  lineelsb2  33163  cvrcmp  35900  cvlatexch3  35955  cvlsupr2  35960  atexchcvrN  36057  3dim1  36084  3dim2  36085  ps-1  36094  ps-2  36095  3atlem3  36102  3atlem5  36104  lplnnle2at  36158  lplnllnneN  36173  2llnjaN  36183  4atlem3  36213  4atlem10b  36222  4atlem12  36229  2llnma3r  36405  paddasslem4  36440  paddasslem7  36443  paddasslem8  36444  paddasslem12  36448  paddasslem13  36449  pmodlem1  36463  pmodlem2  36464  llnexchb2lem  36485  4atex2  36694  ltrnatlw  36800  trlval4  36805  arglem1N  36807  cdlemd4  36818  cdlemd5  36819  cdleme0moN  36842  cdleme16  36902  cdleme20  36941  cdleme21j  36953  cdleme21k  36955  cdleme27N  36986  cdleme28c  36989  cdleme43fsv1snlem  37037  cdleme38n  37081  cdleme40n  37085  cdleme41snaw  37093  cdlemg6c  37237  cdlemg8c  37246  cdlemg8  37248  cdlemg12e  37264  cdlemg16  37274  cdlemg16ALTN  37275  cdlemg16z  37276  cdlemg16zz  37277  cdlemg18a  37295  cdlemg20  37302  cdlemg22  37304  cdlemg37  37306  cdlemg27b  37313  cdlemg31d  37317  cdlemg33  37328  cdlemg38  37332  cdlemg44b  37349  cdlemk38  37532  cdlemk35s-id  37555  cdlemk39s-id  37557  cdlemk55  37578  cdlemk35u  37581  cdlemk55u  37583  cdleml3N  37595  cdlemn11pre  37827