Theorem simpl22 1254

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl22	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl22

Step	Hyp	Ref	Expression
1		simpl2 1194	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl2 1188	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  brbtwn2  26996  ax5seg  27029  axpasch  27032  axeuclid  27054  br8d  30669  br8  33442  cgrextend  34047  segconeq  34049  trisegint  34067  ifscgr  34083  cgrsub  34084  cgrxfr  34094  lineext  34115  seglecgr12im  34149  segletr  34153  lineunray  34186  lineelsb2  34187  cvrcmp  37034  cvlatexch3  37089  cvlsupr2  37094  atcvrj2b  37183  atexchcvrN  37191  3dim1  37218  3dim2  37219  3atlem3  37236  3atlem5  37238  lplnnle2at  37292  2llnjaN  37317  4atlem3  37347  4atlem10b  37356  4atlem12  37363  2llnma3r  37539  paddasslem4  37574  paddasslem7  37577  paddasslem8  37578  paddasslem12  37582  paddasslem13  37583  paddasslem15  37585  pmodlem1  37597  pmodlem2  37598  atmod1i1m  37609  llnexchb2lem  37619  4atex2  37828  ltrnatlw  37934  trlval4  37939  arglem1N  37941  cdlemd4  37952  cdlemd5  37953  cdleme0moN  37976  cdleme16  38036  cdleme20  38075  cdleme21k  38089  cdleme27N  38120  cdleme28c  38123  cdleme43fsv1snlem  38171  cdleme38n  38215  cdleme40n  38219  cdleme41snaw  38227  cdlemg6c  38371  cdlemg8c  38380  cdlemg8  38382  cdlemg12e  38398  cdlemg16  38408  cdlemg16ALTN  38409  cdlemg16z  38410  cdlemg16zz  38411  cdlemg18a  38429  cdlemg20  38436  cdlemg22  38438  cdlemg37  38440  cdlemg31d  38451  cdlemg33  38462  cdlemg38  38466  cdlemg44b  38483  cdlemk38  38666  cdlemk35s-id  38689  cdlemk39s-id  38691  cdlemk53b  38707  cdlemk55  38712  cdlemk35u  38715  cdlemk55u  38717  cdlemn11pre  38961