Theorem simpl21 1270

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  frrlem10  8344  nosupbnd2lem1  28105  noinfbnd2lem1  28120  brbtwn2  29516  ax5seglem3a  29541  ax5seg  29549  axpasch  29552  axeuclid  29574  br8d  33277  br8  36712  cgrextend  36964  segconeq  36966  trisegint  36984  ifscgr  37000  cgrsub  37001  cgrxfr  37011  lineext  37032  seglecgr12im  37066  segletr  37070  lineunray  37103  lineelsb2  37104  cvrcmp  40543  cvlatexch3  40598  cvlsupr2  40603  atexchcvrN  40700  3dim1  40727  3dim2  40728  ps-1  40737  ps-2  40738  3atlem3  40745  3atlem5  40747  lplnnle2at  40801  lplnllnneN  40816  2llnjaN  40826  4atlem3  40856  4atlem10b  40865  4atlem12  40872  2llnma3r  41048  paddasslem4  41083  paddasslem7  41086  paddasslem8  41087  paddasslem12  41091  paddasslem13  41092  pmodlem1  41106  pmodlem2  41107  llnexchb2lem  41128  4atex2  41337  ltrnatlw  41443  trlval4  41448  arglem1N  41450  cdlemd4  41461  cdlemd5  41462  cdleme0moN  41485  cdleme16  41545  cdleme20  41584  cdleme21j  41596  cdleme21k  41598  cdleme27N  41629  cdleme28c  41632  cdleme43fsv1snlem  41680  cdleme38n  41724  cdleme40n  41728  cdleme41snaw  41736  cdlemg6c  41880  cdlemg8c  41889  cdlemg8  41891  cdlemg12e  41907  cdlemg16  41917  cdlemg16ALTN  41918  cdlemg16z  41919  cdlemg16zz  41920  cdlemg18a  41938  cdlemg20  41945  cdlemg22  41947  cdlemg37  41949  cdlemg27b  41956  cdlemg31d  41960  cdlemg33  41971  cdlemg38  41975  cdlemg44b  41992  cdlemk38  42175  cdlemk35s-id  42198  cdlemk39s-id  42200  cdlemk55  42221  cdlemk35u  42224  cdlemk55u  42226  cdleml3N  42238  cdlemn11pre  42470