Theorem simpl12 1250

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl12	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl12

Step	Hyp	Ref	Expression
1		simpl2 1193	. 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  16733  pmatcollpw1lem1  22690  pmatcollpw1  22692  mp2pm2mplem2  22723  nolt02o  27635  nogt01o  27636  brbtwn2  28885  ax5seg  28918  3vfriswmgr  30260  br8  35821  ifscgr  36109  seglecgr12im  36175  lkrshp  39224  atlatle  39439  cvlcvr1  39458  atbtwn  39565  3dimlem3  39580  3dimlem3OLDN  39581  1cvratex  39592  llnmlplnN  39658  4atlem3  39715  4atlem3a  39716  4atlem11  39728  4atlem12  39731  cdlemb  39913  paddasslem4  39942  paddasslem10  39948  pmodlem1  39965  llnexchb2lem  39987  arglem1N  40309  cdlemd4  40320  cdlemd  40326  cdleme16  40404  cdleme20  40443  cdleme21k  40457  cdleme22cN  40461  cdleme27N  40488  cdleme28c  40491  cdleme29ex  40493  cdleme32fva  40556  cdleme40n  40587  cdlemg15a  40774  cdlemg15  40775  cdlemg16ALTN  40777  cdlemg16z  40778  cdlemg20  40804  cdlemg22  40806  cdlemg29  40824  cdlemg38  40834  cdlemk33N  41028  cdlemk56  41090  fourierdlem77  46305