Theorem simpl11 1241

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  pythagtriplem4  15985  tsmsxp  22446  brbtwn2  26374  ax5seg  26407  3vfriswmgr  27749  br8  32600  nolt02o  32808  btwndiff  33097  ifscgr  33114  seglecgr12im  33180  lkrshp  35772  cvlcvr1  36006  atbtwn  36113  3dimlem3  36128  3dimlem3OLDN  36129  1cvratex  36140  llnmlplnN  36206  4atlem3  36263  4atlem3a  36264  4atlem11  36276  4atlem12  36279  lnatexN  36446  cdlemb  36461  paddasslem4  36490  paddasslem10  36496  pmodlem1  36513  llnexchb2lem  36535  llnexchb2  36536  arglem1N  36857  cdlemd4  36868  cdlemd9  36873  cdlemd  36874  cdleme16  36952  cdleme20  36991  cdleme21i  37002  cdleme21k  37005  cdleme27N  37036  cdleme28c  37039  cdlemefrs29bpre0  37063  cdlemefrs29clN  37066  cdlemefrs32fva  37067  cdleme41sn3a  37100  cdleme32fva  37104  cdleme40n  37135  cdlemg12e  37314  cdlemg15a  37322  cdlemg15  37323  cdlemg16ALTN  37325  cdlemg16z  37326  cdlemg20  37352  cdlemg22  37354  cdlemg29  37372  cdlemg38  37382  cdlemk33N  37576  cdlemk56  37638  dihord11b  37889  dihord2pre  37892  dihord4  37925  ismnu  40094  fourierdlem77  42010