Theorem simpl22 1251

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 1191	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl2 1185	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:  brbtwn2  28934  ax5seg  28967  axpasch  28970  axeuclid  28992  br8d  32629  br8  35735  cgrextend  35989  segconeq  35991  trisegint  36009  ifscgr  36025  cgrsub  36026  cgrxfr  36036  lineext  36057  seglecgr12im  36091  segletr  36095  lineunray  36128  lineelsb2  36129  cvrcmp  39264  cvlatexch3  39319  cvlsupr2  39324  atcvrj2b  39414  atexchcvrN  39422  3dim1  39449  3dim2  39450  3atlem3  39467  3atlem5  39469  lplnnle2at  39523  2llnjaN  39548  4atlem3  39578  4atlem10b  39587  4atlem12  39594  2llnma3r  39770  paddasslem4  39805  paddasslem7  39808  paddasslem8  39809  paddasslem12  39813  paddasslem13  39814  paddasslem15  39816  pmodlem1  39828  pmodlem2  39829  atmod1i1m  39840  llnexchb2lem  39850  4atex2  40059  ltrnatlw  40165  trlval4  40170  arglem1N  40172  cdlemd4  40183  cdlemd5  40184  cdleme0moN  40207  cdleme16  40267  cdleme20  40306  cdleme21k  40320  cdleme27N  40351  cdleme28c  40354  cdleme43fsv1snlem  40402  cdleme38n  40446  cdleme40n  40450  cdleme41snaw  40458  cdlemg6c  40602  cdlemg8c  40611  cdlemg8  40613  cdlemg12e  40629  cdlemg16  40639  cdlemg16ALTN  40640  cdlemg16z  40641  cdlemg16zz  40642  cdlemg18a  40660  cdlemg20  40667  cdlemg22  40669  cdlemg37  40671  cdlemg31d  40682  cdlemg33  40693  cdlemg38  40697  cdlemg44b  40714  cdlemk38  40897  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk53b  40938  cdlemk55  40943  cdlemk35u  40946  cdlemk55u  40948  cdlemn11pre  41192