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  27626  noinfres  27641  ax5seglem3a  28864  ax5seg  28872  uhgrwkspth  29692  usgr2wlkspth  29696  br8d  32545  br8  35750  cgrextend  36003  segconeq  36005  trisegint  36023  ifscgr  36039  cgrsub  36040  btwnxfr  36051  seglecgr12im  36105  segletr  36109  atbtwn  39447  3dim1  39468  2llnjaN  39567  4atlem10b  39606  4atlem11  39610  4atlem12  39613  2lplnj  39621  paddasslem4  39824  pmodlem1  39847  4atex2  40078  trlval3  40188  arglem1N  40191  cdleme0moN  40226  cdleme17b  40288  cdleme20  40325  cdleme21j  40337  cdleme28c  40373  cdleme35h2  40458  cdlemg6c  40621  cdlemg6  40624  cdlemg7N  40627  cdlemg8c  40630  cdlemg11a  40638  cdlemg11b  40643  cdlemg12e  40648  cdlemg16  40658  cdlemg16ALTN  40659  cdlemg16zz  40661  cdlemg20  40686  cdlemg22  40688  cdlemg37  40690  cdlemg31d  40701  cdlemg33b  40708  cdlemg33  40712  cdlemg39  40717  cdlemg42  40730  cdlemk25-3  40905  cdlemk33N  40910  cdlemk53b  40957