Theorem simpl11 1249

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 1192	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl1 1186	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  16797  tsmsxp  24049  nolt02o  27614  nogt01o  27615  cofsslt  27833  brbtwn2  28839  ax5seg  28872  3vfriswmgr  30214  br8  35750  btwndiff  36022  ifscgr  36039  seglecgr12im  36105  lkrshp  39105  cvlcvr1  39339  atbtwn  39447  3dimlem3  39462  3dimlem3OLDN  39463  1cvratex  39474  llnmlplnN  39540  4atlem3  39597  4atlem3a  39598  4atlem11  39610  4atlem12  39613  lnatexN  39780  cdlemb  39795  paddasslem4  39824  paddasslem10  39830  pmodlem1  39847  llnexchb2lem  39869  llnexchb2  39870  arglem1N  40191  cdlemd4  40202  cdlemd9  40207  cdlemd  40208  cdleme16  40286  cdleme20  40325  cdleme21i  40336  cdleme21k  40339  cdleme27N  40370  cdleme28c  40373  cdlemefrs29bpre0  40397  cdlemefrs29clN  40400  cdlemefrs32fva  40401  cdleme41sn3a  40434  cdleme32fva  40438  cdleme40n  40469  cdlemg12e  40648  cdlemg15a  40656  cdlemg15  40657  cdlemg16ALTN  40659  cdlemg16z  40660  cdlemg20  40686  cdlemg22  40688  cdlemg29  40706  cdlemg38  40716  cdlemk33N  40910  cdlemk56  40972  dihord11b  41223  dihord2pre  41226  dihord4  41259  ismnu  44257  fourierdlem77  46188