Theorem simpl12 1249

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pythagtriplem4  16866  pmatcollpw1lem1  22801  pmatcollpw1  22803  mp2pm2mplem2  22834  nolt02o  27758  nogt01o  27759  brbtwn2  28938  ax5seg  28971  3vfriswmgr  30310  br8  35718  ifscgr  36008  seglecgr12im  36074  lkrshp  39061  atlatle  39276  cvlcvr1  39295  atbtwn  39403  3dimlem3  39418  3dimlem3OLDN  39419  1cvratex  39430  llnmlplnN  39496  4atlem3  39553  4atlem3a  39554  4atlem11  39566  4atlem12  39569  cdlemb  39751  paddasslem4  39780  paddasslem10  39786  pmodlem1  39803  llnexchb2lem  39825  arglem1N  40147  cdlemd4  40158  cdlemd  40164  cdleme16  40242  cdleme20  40281  cdleme21k  40295  cdleme22cN  40299  cdleme27N  40326  cdleme28c  40329  cdleme29ex  40331  cdleme32fva  40394  cdleme40n  40425  cdlemg15a  40612  cdlemg15  40613  cdlemg16ALTN  40615  cdlemg16z  40616  cdlemg20  40642  cdlemg22  40644  cdlemg29  40662  cdlemg38  40672  cdlemk33N  40866  cdlemk56  40928  fourierdlem77  46104