Theorem simpl21 1321

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  brbtwn2  26005  ax5seglem3a  26030  ax5seg  26038  axpasch  26041  axeuclid  26063  br8d  29750  br8  31974  nosupbnd2lem1  32188  cgrextend  32442  segconeq  32444  trisegint  32462  ifscgr  32478  cgrsub  32479  cgrxfr  32489  lineext  32510  seglecgr12im  32544  segletr  32548  lineunray  32581  lineelsb2  32582  cvrcmp  35091  cvlatexch3  35146  cvlsupr2  35151  atexchcvrN  35247  3dim1  35274  3dim2  35275  ps-1  35284  ps-2  35285  3atlem3  35292  3atlem5  35294  lplnnle2at  35348  lplnllnneN  35363  2llnjaN  35373  4atlem3  35403  4atlem10b  35412  4atlem12  35419  2llnma3r  35595  paddasslem4  35630  paddasslem7  35633  paddasslem8  35634  paddasslem12  35638  paddasslem13  35639  pmodlem1  35653  pmodlem2  35654  llnexchb2lem  35675  4atex2  35884  ltrnatlw  35991  trlval4  35996  arglem1N  35998  cdlemd4  36009  cdlemd5  36010  cdleme0moN  36033  cdleme16  36093  cdleme20  36132  cdleme21j  36144  cdleme21k  36146  cdleme27N  36177  cdleme28c  36180  cdleme43fsv1snlem  36228  cdleme38n  36272  cdleme40n  36276  cdleme41snaw  36284  cdlemg6c  36428  cdlemg8c  36437  cdlemg8  36439  cdlemg12e  36455  cdlemg16  36465  cdlemg16ALTN  36466  cdlemg16z  36467  cdlemg16zz  36468  cdlemg18a  36486  cdlemg20  36493  cdlemg22  36495  cdlemg37  36497  cdlemg27b  36504  cdlemg31d  36508  cdlemg33  36519  cdlemg38  36523  cdlemg44b  36540  cdlemk38  36723  cdlemk35s-id  36746  cdlemk39s-id  36748  cdlemk55  36769  cdlemk35u  36772  cdlemk55u  36774  cdleml3N  36786  cdlemn11pre  37019