Theorem simpl33 1257

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

Assertion

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

Proof of Theorem simpl33

Step	Hyp	Ref	Expression
1		simpl3 1194	. 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:  nosupres  27675  noinfres  27690  ax5seglem3a  29003  ax5seg  29011  numclwwlk1lem2foa  30429  br8d  32686  br8  35950  cgrextend  36202  segconeq  36204  trisegint  36222  ifscgr  36238  cgrsub  36239  btwnxfr  36250  seglecgr12im  36304  segletr  36308  atbtwn  39706  4atlem10b  39865  4atlem11  39869  4atlem12  39872  2lplnj  39880  paddasslem4  40083  paddasslem7  40086  pmodlem1  40106  4atex2  40337  trlval3  40447  arglem1N  40450  cdleme0moN  40485  cdleme20  40584  cdleme21j  40596  cdleme28c  40632  cdleme38n  40724  cdlemg6c  40880  cdlemg6  40883  cdlemg7N  40886  cdlemg16  40917  cdlemg16ALTN  40918  cdlemg16zz  40920  cdlemg20  40945  cdlemg22  40947  cdlemg37  40949  cdlemg31d  40960  cdlemg29  40965  cdlemg33b  40967  cdlemg33  40971  cdlemg46  40995  cdlemk25-3  41164