Theorem simpl22 1253

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 1193	. 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:  brbtwn2  28839  ax5seg  28872  axpasch  28875  axeuclid  28897  br8d  32545  br8  35750  cgrextend  36003  segconeq  36005  trisegint  36023  ifscgr  36039  cgrsub  36040  cgrxfr  36050  lineext  36071  seglecgr12im  36105  segletr  36109  lineunray  36142  lineelsb2  36143  cvrcmp  39283  cvlatexch3  39338  cvlsupr2  39343  atcvrj2b  39433  atexchcvrN  39441  3dim1  39468  3dim2  39469  3atlem3  39486  3atlem5  39488  lplnnle2at  39542  2llnjaN  39567  4atlem3  39597  4atlem10b  39606  4atlem12  39613  2llnma3r  39789  paddasslem4  39824  paddasslem7  39827  paddasslem8  39828  paddasslem12  39832  paddasslem13  39833  paddasslem15  39835  pmodlem1  39847  pmodlem2  39848  atmod1i1m  39859  llnexchb2lem  39869  4atex2  40078  ltrnatlw  40184  trlval4  40189  arglem1N  40191  cdlemd4  40202  cdlemd5  40203  cdleme0moN  40226  cdleme16  40286  cdleme20  40325  cdleme21k  40339  cdleme27N  40370  cdleme28c  40373  cdleme43fsv1snlem  40421  cdleme38n  40465  cdleme40n  40469  cdleme41snaw  40477  cdlemg6c  40621  cdlemg8c  40630  cdlemg8  40632  cdlemg12e  40648  cdlemg16  40658  cdlemg16ALTN  40659  cdlemg16z  40660  cdlemg16zz  40661  cdlemg18a  40679  cdlemg20  40686  cdlemg22  40688  cdlemg37  40690  cdlemg31d  40701  cdlemg33  40712  cdlemg38  40716  cdlemg44b  40733  cdlemk38  40916  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk53b  40957  cdlemk55  40962  cdlemk35u  40965  cdlemk55u  40967  cdlemn11pre  41211