Theorem simpl11 1248

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

Assertion

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

Proof of Theorem simpl11

Step	Hyp	Ref	Expression
1		simpl1 1191	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl1 1185	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:  pythagtriplem4  16840  tsmsxp  24110  nolt02o  27677  nogt01o  27678  cofsslt  27889  brbtwn2  28851  ax5seg  28884  3vfriswmgr  30226  br8  35731  btwndiff  36003  ifscgr  36020  seglecgr12im  36086  lkrshp  39081  cvlcvr1  39315  atbtwn  39423  3dimlem3  39438  3dimlem3OLDN  39439  1cvratex  39450  llnmlplnN  39516  4atlem3  39573  4atlem3a  39574  4atlem11  39586  4atlem12  39589  lnatexN  39756  cdlemb  39771  paddasslem4  39800  paddasslem10  39806  pmodlem1  39823  llnexchb2lem  39845  llnexchb2  39846  arglem1N  40167  cdlemd4  40178  cdlemd9  40183  cdlemd  40184  cdleme16  40262  cdleme20  40301  cdleme21i  40312  cdleme21k  40315  cdleme27N  40346  cdleme28c  40349  cdlemefrs29bpre0  40373  cdlemefrs29clN  40376  cdlemefrs32fva  40377  cdleme41sn3a  40410  cdleme32fva  40414  cdleme40n  40445  cdlemg12e  40624  cdlemg15a  40632  cdlemg15  40633  cdlemg16ALTN  40635  cdlemg16z  40636  cdlemg20  40662  cdlemg22  40664  cdlemg29  40682  cdlemg38  40692  cdlemk33N  40886  cdlemk56  40948  dihord11b  41199  dihord2pre  41202  dihord4  41235  ismnu  44252  fourierdlem77  46170