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  8225  nosupbnd2lem1  27652  noinfbnd2lem1  27667  brbtwn2  28881  ax5seglem3a  28906  ax5seg  28914  axpasch  28917  axeuclid  28939  br8d  32586  br8  35788  cgrextend  36041  segconeq  36043  trisegint  36061  ifscgr  36077  cgrsub  36078  cgrxfr  36088  lineext  36109  seglecgr12im  36143  segletr  36147  lineunray  36180  lineelsb2  36181  cvrcmp  39321  cvlatexch3  39376  cvlsupr2  39381  atexchcvrN  39478  3dim1  39505  3dim2  39506  ps-1  39515  ps-2  39516  3atlem3  39523  3atlem5  39525  lplnnle2at  39579  lplnllnneN  39594  2llnjaN  39604  4atlem3  39634  4atlem10b  39643  4atlem12  39650  2llnma3r  39826  paddasslem4  39861  paddasslem7  39864  paddasslem8  39865  paddasslem12  39869  paddasslem13  39870  pmodlem1  39884  pmodlem2  39885  llnexchb2lem  39906  4atex2  40115  ltrnatlw  40221  trlval4  40226  arglem1N  40228  cdlemd4  40239  cdlemd5  40240  cdleme0moN  40263  cdleme16  40323  cdleme20  40362  cdleme21j  40374  cdleme21k  40376  cdleme27N  40407  cdleme28c  40410  cdleme43fsv1snlem  40458  cdleme38n  40502  cdleme40n  40506  cdleme41snaw  40514  cdlemg6c  40658  cdlemg8c  40667  cdlemg8  40669  cdlemg12e  40685  cdlemg16  40695  cdlemg16ALTN  40696  cdlemg16z  40697  cdlemg16zz  40698  cdlemg18a  40716  cdlemg20  40723  cdlemg22  40725  cdlemg37  40727  cdlemg27b  40734  cdlemg31d  40738  cdlemg33  40749  cdlemg38  40753  cdlemg44b  40770  cdlemk38  40953  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk55  40999  cdlemk35u  41002  cdlemk55u  41004  cdleml3N  41016  cdlemn11pre  41248