Theorem simpl11 1244

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 1187	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl1 1181	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pythagtriplem4  16150  tsmsxp  22757  brbtwn2  26685  ax5seg  26718  3vfriswmgr  28051  br8  32987  nolt02o  33194  btwndiff  33483  ifscgr  33500  seglecgr12im  33566  lkrshp  36235  cvlcvr1  36469  atbtwn  36576  3dimlem3  36591  3dimlem3OLDN  36592  1cvratex  36603  llnmlplnN  36669  4atlem3  36726  4atlem3a  36727  4atlem11  36739  4atlem12  36742  lnatexN  36909  cdlemb  36924  paddasslem4  36953  paddasslem10  36959  pmodlem1  36976  llnexchb2lem  36998  llnexchb2  36999  arglem1N  37320  cdlemd4  37331  cdlemd9  37336  cdlemd  37337  cdleme16  37415  cdleme20  37454  cdleme21i  37465  cdleme21k  37468  cdleme27N  37499  cdleme28c  37502  cdlemefrs29bpre0  37526  cdlemefrs29clN  37529  cdlemefrs32fva  37530  cdleme41sn3a  37563  cdleme32fva  37567  cdleme40n  37598  cdlemg12e  37777  cdlemg15a  37785  cdlemg15  37786  cdlemg16ALTN  37788  cdlemg16z  37789  cdlemg20  37815  cdlemg22  37817  cdlemg29  37835  cdlemg38  37845  cdlemk33N  38039  cdlemk56  38101  dihord11b  38352  dihord2pre  38355  dihord4  38388  ismnu  40590  fourierdlem77  42461