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  8292  nosupbnd2lem1  27677  noinfbnd2lem1  27692  brbtwn2  28830  ax5seglem3a  28855  ax5seg  28863  axpasch  28866  axeuclid  28888  br8d  32536  br8  35719  cgrextend  35972  segconeq  35974  trisegint  35992  ifscgr  36008  cgrsub  36009  cgrxfr  36019  lineext  36040  seglecgr12im  36074  segletr  36078  lineunray  36111  lineelsb2  36112  cvrcmp  39247  cvlatexch3  39302  cvlsupr2  39307  atexchcvrN  39405  3dim1  39432  3dim2  39433  ps-1  39442  ps-2  39443  3atlem3  39450  3atlem5  39452  lplnnle2at  39506  lplnllnneN  39521  2llnjaN  39531  4atlem3  39561  4atlem10b  39570  4atlem12  39577  2llnma3r  39753  paddasslem4  39788  paddasslem7  39791  paddasslem8  39792  paddasslem12  39796  paddasslem13  39797  pmodlem1  39811  pmodlem2  39812  llnexchb2lem  39833  4atex2  40042  ltrnatlw  40148  trlval4  40153  arglem1N  40155  cdlemd4  40166  cdlemd5  40167  cdleme0moN  40190  cdleme16  40250  cdleme20  40289  cdleme21j  40301  cdleme21k  40303  cdleme27N  40334  cdleme28c  40337  cdleme43fsv1snlem  40385  cdleme38n  40429  cdleme40n  40433  cdleme41snaw  40441  cdlemg6c  40585  cdlemg8c  40594  cdlemg8  40596  cdlemg12e  40612  cdlemg16  40622  cdlemg16ALTN  40623  cdlemg16z  40624  cdlemg16zz  40625  cdlemg18a  40643  cdlemg20  40650  cdlemg22  40652  cdlemg37  40654  cdlemg27b  40661  cdlemg31d  40665  cdlemg33  40676  cdlemg38  40680  cdlemg44b  40697  cdlemk38  40880  cdlemk35s-id  40903  cdlemk39s-id  40905  cdlemk55  40926  cdlemk35u  40929  cdlemk55u  40931  cdleml3N  40943  cdlemn11pre  41175