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  16747  pmatcollpw1lem1  22718  pmatcollpw1  22720  mp2pm2mplem2  22751  nolt02o  27663  nogt01o  27664  brbtwn2  28978  ax5seg  29011  3vfriswmgr  30353  br8  35950  ifscgr  36238  seglecgr12im  36304  lkrshp  39361  atlatle  39576  cvlcvr1  39595  atbtwn  39702  3dimlem3  39717  3dimlem3OLDN  39718  1cvratex  39729  llnmlplnN  39795  4atlem3  39852  4atlem3a  39853  4atlem11  39865  4atlem12  39868  cdlemb  40050  paddasslem4  40079  paddasslem10  40085  pmodlem1  40102  llnexchb2lem  40124  arglem1N  40446  cdlemd4  40457  cdlemd  40463  cdleme16  40541  cdleme20  40580  cdleme21k  40594  cdleme22cN  40598  cdleme27N  40625  cdleme28c  40628  cdleme29ex  40630  cdleme32fva  40693  cdleme40n  40724  cdlemg15a  40911  cdlemg15  40912  cdlemg16ALTN  40914  cdlemg16z  40915  cdlemg20  40941  cdlemg22  40943  cdlemg29  40961  cdlemg38  40971  cdlemk33N  41165  cdlemk56  41227  fourierdlem77  46423