Theorem simpl12 1248

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pythagtriplem4  16594  pmatcollpw1lem1  22003  pmatcollpw1  22005  mp2pm2mplem2  22036  brbtwn2  27406  ax5seg  27439  3vfriswmgr  28774  br8  33853  poxp3  33922  nolt02o  33968  nogt01o  33969  ifscgr  34416  seglecgr12im  34482  lkrshp  37344  atlatle  37559  cvlcvr1  37578  atbtwn  37686  3dimlem3  37701  3dimlem3OLDN  37702  1cvratex  37713  llnmlplnN  37779  4atlem3  37836  4atlem3a  37837  4atlem11  37849  4atlem12  37852  cdlemb  38034  paddasslem4  38063  paddasslem10  38069  pmodlem1  38086  llnexchb2lem  38108  arglem1N  38430  cdlemd4  38441  cdlemd  38447  cdleme16  38525  cdleme20  38564  cdleme21k  38578  cdleme22cN  38582  cdleme27N  38609  cdleme28c  38612  cdleme29ex  38614  cdleme32fva  38677  cdleme40n  38708  cdlemg15a  38895  cdlemg15  38896  cdlemg16ALTN  38898  cdlemg16z  38899  cdlemg20  38925  cdlemg22  38927  cdlemg29  38945  cdlemg38  38955  cdlemk33N  39149  cdlemk56  39211  fourierdlem77  43979