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  17003  tsmsxp  24480  nolt02o  28058  nogt01o  28059  cofslts  28310  brbtwn2  29489  ax5seg  29522  3vfriswmgr  30885  br8  36614  btwndiff  36885  ifscgr  36902  seglecgr12im  36968  lkrshp  40256  cvlcvr1  40490  atbtwn  40597  3dimlem3  40612  3dimlem3OLDN  40613  1cvratex  40624  llnmlplnN  40690  4atlem3  40747  4atlem3a  40748  4atlem11  40760  4atlem12  40763  lnatexN  40930  cdlemb  40945  paddasslem4  40974  paddasslem10  40980  pmodlem1  40997  llnexchb2lem  41019  llnexchb2  41020  arglem1N  41341  cdlemd4  41352  cdlemd9  41357  cdlemd  41358  cdleme16  41436  cdleme20  41475  cdleme21i  41486  cdleme21k  41489  cdleme27N  41520  cdleme28c  41523  cdlemefrs29bpre0  41547  cdlemefrs29clN  41550  cdlemefrs32fva  41551  cdleme41sn3a  41584  cdleme32fva  41588  cdleme40n  41619  cdlemg12e  41798  cdlemg15a  41806  cdlemg15  41807  cdlemg16ALTN  41809  cdlemg16z  41810  cdlemg20  41836  cdlemg22  41838  cdlemg29  41856  cdlemg38  41866  cdlemk33N  42060  cdlemk56  42122  dihord11b  42373  dihord2pre  42376  dihord4  42409  ismnu  45339  fourierdlem77  47287