Theorem simpl32 1256

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

Assertion

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

Proof of Theorem simpl32

Step	Hyp	Ref	Expression
1		simpl2 1193	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl3 1188	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:  initoeu2lem2  17939  mulmarep1gsum2  22518  tsmsxp  24099  noinfres  27690  ax5seg  29011  br8d  32686  br8  35950  cgrextend  36202  segconeq  36204  trisegint  36222  ifscgr  36238  cgrsub  36239  btwnxfr  36250  seglecgr12im  36304  segletr  36308  exatleN  39660  atbtwn  39702  3dim1  39723  3dim2  39724  2llnjaN  39822  4atlem10b  39861  4atlem11  39865  4atlem12  39868  2lplnj  39876  cdlemb  40050  paddasslem4  40079  pmodlem1  40102  4atex2  40333  trlval3  40443  arglem1N  40446  cdleme0moN  40481  cdleme17b  40543  cdleme20  40580  cdleme21j  40592  cdleme28c  40628  cdleme35h2  40713  cdleme38n  40720  cdlemg6c  40876  cdlemg6  40879  cdlemg7N  40882  cdlemg11a  40893  cdlemg12e  40903  cdlemg16  40913  cdlemg16ALTN  40914  cdlemg16zz  40916  cdlemg20  40941  cdlemg22  40943  cdlemg37  40945  cdlemg31d  40956  cdlemg29  40961  cdlemg33b  40963  cdlemg33  40967  cdlemg39  40972  cdlemg42  40985  cdlemk25-3  41160