Theorem simpl31 1255

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

Assertion

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

Proof of Theorem simpl31

Step	Hyp	Ref	Expression
1		simpl1 1192	. 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  uhgrwkspth  29828  usgr2wlkspth  29832  br8d  32686  br8  35950  cgrextend  36202  segconeq  36204  trisegint  36222  ifscgr  36238  cgrsub  36239  btwnxfr  36250  seglecgr12im  36304  segletr  36308  atbtwn  39706  3dim1  39727  2llnjaN  39826  4atlem10b  39865  4atlem11  39869  4atlem12  39872  2lplnj  39880  paddasslem4  40083  pmodlem1  40106  4atex2  40337  trlval3  40447  arglem1N  40450  cdleme0moN  40485  cdleme17b  40547  cdleme20  40584  cdleme21j  40596  cdleme28c  40632  cdleme35h2  40717  cdlemg6c  40880  cdlemg6  40883  cdlemg7N  40886  cdlemg8c  40889  cdlemg11a  40897  cdlemg11b  40902  cdlemg12e  40907  cdlemg16  40917  cdlemg16ALTN  40918  cdlemg16zz  40920  cdlemg20  40945  cdlemg22  40947  cdlemg37  40949  cdlemg31d  40960  cdlemg33b  40967  cdlemg33  40971  cdlemg39  40976  cdlemg42  40989  cdlemk25-3  41164  cdlemk33N  41169  cdlemk53b  41216