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  16977  tsmsxp  24454  nolt02o  28034  nogt01o  28035  cofslts  28286  brbtwn2  29465  ax5seg  29498  3vfriswmgr  30861  br8  36490  btwndiff  36762  ifscgr  36779  seglecgr12im  36845  lkrshp  40130  cvlcvr1  40364  atbtwn  40471  3dimlem3  40486  3dimlem3OLDN  40487  1cvratex  40498  llnmlplnN  40564  4atlem3  40621  4atlem3a  40622  4atlem11  40634  4atlem12  40637  lnatexN  40804  cdlemb  40819  paddasslem4  40848  paddasslem10  40854  pmodlem1  40871  llnexchb2lem  40893  llnexchb2  40894  arglem1N  41215  cdlemd4  41226  cdlemd9  41231  cdlemd  41232  cdleme16  41310  cdleme20  41349  cdleme21i  41360  cdleme21k  41363  cdleme27N  41394  cdleme28c  41397  cdlemefrs29bpre0  41421  cdlemefrs29clN  41424  cdlemefrs32fva  41425  cdleme41sn3a  41458  cdleme32fva  41462  cdleme40n  41493  cdlemg12e  41672  cdlemg15a  41680  cdlemg15  41681  cdlemg16ALTN  41683  cdlemg16z  41684  cdlemg20  41710  cdlemg22  41712  cdlemg29  41730  cdlemg38  41740  cdlemk33N  41934  cdlemk56  41996  dihord11b  42247  dihord2pre  42250  dihord4  42283  ismnu  45204  fourierdlem77  47137