Theorem simpl11 1247

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 1190	. 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  16529  tsmsxp  23315  brbtwn2  27282  ax5seg  27315  3vfriswmgr  28651  br8  33732  poxp3  33805  nolt02o  33907  nogt01o  33908  cofsslt  34097  btwndiff  34338  ifscgr  34355  seglecgr12im  34421  lkrshp  37126  cvlcvr1  37360  atbtwn  37467  3dimlem3  37482  3dimlem3OLDN  37483  1cvratex  37494  llnmlplnN  37560  4atlem3  37617  4atlem3a  37618  4atlem11  37630  4atlem12  37633  lnatexN  37800  cdlemb  37815  paddasslem4  37844  paddasslem10  37850  pmodlem1  37867  llnexchb2lem  37889  llnexchb2  37890  arglem1N  38211  cdlemd4  38222  cdlemd9  38227  cdlemd  38228  cdleme16  38306  cdleme20  38345  cdleme21i  38356  cdleme21k  38359  cdleme27N  38390  cdleme28c  38393  cdlemefrs29bpre0  38417  cdlemefrs29clN  38420  cdlemefrs32fva  38421  cdleme41sn3a  38454  cdleme32fva  38458  cdleme40n  38489  cdlemg12e  38668  cdlemg15a  38676  cdlemg15  38677  cdlemg16ALTN  38679  cdlemg16z  38680  cdlemg20  38706  cdlemg22  38708  cdlemg29  38726  cdlemg38  38736  cdlemk33N  38930  cdlemk56  38992  dihord11b  39243  dihord2pre  39246  dihord4  39279  ismnu  41886  fourierdlem77  43731