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  16837  pmatcollpw1lem1  22710  pmatcollpw1  22712  mp2pm2mplem2  22743  nolt02o  27657  nogt01o  27658  brbtwn2  28830  ax5seg  28863  3vfriswmgr  30205  br8  35719  ifscgr  36008  seglecgr12im  36074  lkrshp  39069  atlatle  39284  cvlcvr1  39303  atbtwn  39411  3dimlem3  39426  3dimlem3OLDN  39427  1cvratex  39438  llnmlplnN  39504  4atlem3  39561  4atlem3a  39562  4atlem11  39574  4atlem12  39577  cdlemb  39759  paddasslem4  39788  paddasslem10  39794  pmodlem1  39811  llnexchb2lem  39833  arglem1N  40155  cdlemd4  40166  cdlemd  40172  cdleme16  40250  cdleme20  40289  cdleme21k  40303  cdleme22cN  40307  cdleme27N  40334  cdleme28c  40337  cdleme29ex  40339  cdleme32fva  40402  cdleme40n  40433  cdlemg15a  40620  cdlemg15  40621  cdlemg16ALTN  40623  cdlemg16z  40624  cdlemg20  40650  cdlemg22  40652  cdlemg29  40670  cdlemg38  40680  cdlemk33N  40874  cdlemk56  40936  fourierdlem77  46160