Theorem simpl11 1267

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pythagtriplem4  16904  tsmsxp  24349  nolt02o  27896  nogt01o  27897  cofslts  28148  brbtwn2  29292  ax5seg  29325  3vfriswmgr  30666  br8  36269  btwndiff  36540  ifscgr  36557  seglecgr12im  36623  lkrshp  39920  cvlcvr1  40154  atbtwn  40261  3dimlem3  40276  3dimlem3OLDN  40277  1cvratex  40288  llnmlplnN  40354  4atlem3  40411  4atlem3a  40412  4atlem11  40424  4atlem12  40427  lnatexN  40594  cdlemb  40609  paddasslem4  40638  paddasslem10  40644  pmodlem1  40661  llnexchb2lem  40683  llnexchb2  40684  arglem1N  41005  cdlemd4  41016  cdlemd9  41021  cdlemd  41022  cdleme16  41100  cdleme20  41139  cdleme21i  41150  cdleme21k  41153  cdleme27N  41184  cdleme28c  41187  cdlemefrs29bpre0  41211  cdlemefrs29clN  41214  cdlemefrs32fva  41215  cdleme41sn3a  41248  cdleme32fva  41252  cdleme40n  41283  cdlemg12e  41462  cdlemg15a  41470  cdlemg15  41471  cdlemg16ALTN  41473  cdlemg16z  41474  cdlemg20  41500  cdlemg22  41502  cdlemg29  41520  cdlemg38  41530  cdlemk33N  41724  cdlemk56  41786  dihord11b  42037  dihord2pre  42040  dihord4  42073  ismnu  45012  fourierdlem77  46938