Theorem simpl21 1258

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

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

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 1094

This theorem is referenced by:  frrlem10  8242  nosupbnd2lem1  27704  noinfbnd2lem1  27719  brbtwn2  28999  ax5seglem3a  29024  ax5seg  29032  axpasch  29035  axeuclid  29057  br8d  32707  br8  35991  cgrextend  36243  segconeq  36245  trisegint  36263  ifscgr  36279  cgrsub  36280  cgrxfr  36290  lineext  36311  seglecgr12im  36345  segletr  36349  lineunray  36382  lineelsb2  36383  cvrcmp  39782  cvlatexch3  39837  cvlsupr2  39842  atexchcvrN  39939  3dim1  39966  3dim2  39967  ps-1  39976  ps-2  39977  3atlem3  39984  3atlem5  39986  lplnnle2at  40040  lplnllnneN  40055  2llnjaN  40065  4atlem3  40095  4atlem10b  40104  4atlem12  40111  2llnma3r  40287  paddasslem4  40322  paddasslem7  40325  paddasslem8  40326  paddasslem12  40330  paddasslem13  40331  pmodlem1  40345  pmodlem2  40346  llnexchb2lem  40367  4atex2  40576  ltrnatlw  40682  trlval4  40687  arglem1N  40689  cdlemd4  40700  cdlemd5  40701  cdleme0moN  40724  cdleme16  40784  cdleme20  40823  cdleme21j  40835  cdleme21k  40837  cdleme27N  40868  cdleme28c  40871  cdleme43fsv1snlem  40919  cdleme38n  40963  cdleme40n  40967  cdleme41snaw  40975  cdlemg6c  41119  cdlemg8c  41128  cdlemg8  41130  cdlemg12e  41146  cdlemg16  41156  cdlemg16ALTN  41157  cdlemg16z  41158  cdlemg16zz  41159  cdlemg18a  41177  cdlemg20  41184  cdlemg22  41186  cdlemg37  41188  cdlemg27b  41195  cdlemg31d  41199  cdlemg33  41210  cdlemg38  41214  cdlemg44b  41231  cdlemk38  41414  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk55  41460  cdlemk35u  41463  cdlemk55u  41465  cdleml3N  41477  cdlemn11pre  41709