Theorem simpl11 1249

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl11	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑)

Proof of Theorem simpl11

Step	Hyp	Ref	Expression
1		simpl1 1192	. 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  tsmsxp  24099  nolt02o  27663  nogt01o  27664  cofslts  27914  brbtwn2  28978  ax5seg  29011  3vfriswmgr  30353  br8  35950  btwndiff  36221  ifscgr  36238  seglecgr12im  36304  lkrshp  39361  cvlcvr1  39595  atbtwn  39702  3dimlem3  39717  3dimlem3OLDN  39718  1cvratex  39729  llnmlplnN  39795  4atlem3  39852  4atlem3a  39853  4atlem11  39865  4atlem12  39868  lnatexN  40035  cdlemb  40050  paddasslem4  40079  paddasslem10  40085  pmodlem1  40102  llnexchb2lem  40124  llnexchb2  40125  arglem1N  40446  cdlemd4  40457  cdlemd9  40462  cdlemd  40463  cdleme16  40541  cdleme20  40580  cdleme21i  40591  cdleme21k  40594  cdleme27N  40625  cdleme28c  40628  cdlemefrs29bpre0  40652  cdlemefrs29clN  40655  cdlemefrs32fva  40656  cdleme41sn3a  40689  cdleme32fva  40693  cdleme40n  40724  cdlemg12e  40903  cdlemg15a  40911  cdlemg15  40912  cdlemg16ALTN  40914  cdlemg16z  40915  cdlemg20  40941  cdlemg22  40943  cdlemg29  40961  cdlemg38  40971  cdlemk33N  41165  cdlemk56  41227  dihord11b  41478  dihord2pre  41481  dihord4  41514  ismnu  44498  fourierdlem77  46423