Theorem simpl12 1246

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  pythagtriplem4  16146  pmatcollpw1lem1  21379  pmatcollpw1  21381  mp2pm2mplem2  21412  brbtwn2  26699  ax5seg  26732  3vfriswmgr  28063  br8  33105  nolt02o  33312  ifscgr  33618  seglecgr12im  33684  lkrshp  36401  atlatle  36616  cvlcvr1  36635  atbtwn  36742  3dimlem3  36757  3dimlem3OLDN  36758  1cvratex  36769  llnmlplnN  36835  4atlem3  36892  4atlem3a  36893  4atlem11  36905  4atlem12  36908  cdlemb  37090  paddasslem4  37119  paddasslem10  37125  pmodlem1  37142  llnexchb2lem  37164  arglem1N  37486  cdlemd4  37497  cdlemd  37503  cdleme16  37581  cdleme20  37620  cdleme21k  37634  cdleme22cN  37638  cdleme27N  37665  cdleme28c  37668  cdleme29ex  37670  cdleme32fva  37733  cdleme40n  37764  cdlemg15a  37951  cdlemg15  37952  cdlemg16ALTN  37954  cdlemg16z  37955  cdlemg20  37981  cdlemg22  37983  cdlemg29  38001  cdlemg38  38011  cdlemk33N  38205  cdlemk56  38267  fourierdlem77  42825