Theorem simp3ll 1245

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

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

Proof of Theorem simp3ll

Step	Hyp	Ref	Expression
1		simpll 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant3 1136	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  f1oiso2  7349  omeu  8585  ntrivcvgmul  15848  tsmsxp  23659  tgqioo  24316  ovolunlem2  25015  plyadd  25731  plymul  25732  coeeu  25739  nosupbnd1lem2  27212  noinfbnd1lem2  27227  tghilberti2  27889  btwnconn1lem2  35060  btwnconn1lem3  35061  btwnconn1lem12  35070  athgt  38327  2llnjN  38438  4atlem12b  38482  lncmp  38654  cdlema2N  38663  cdlemc2  39063  cdleme5  39111  cdleme11a  39131  cdleme21ct  39200  cdleme21  39208  cdleme22eALTN  39216  cdleme24  39223  cdleme27cl  39237  cdleme27a  39238  cdleme28  39244  cdleme36a  39331  cdleme42b  39349  cdleme48fvg  39371  cdlemf  39434  cdlemk39  39787  cdlemkid1  39793  dihlsscpre  40105  dihord4  40129  dihord5apre  40133  dihmeetlem20N  40197  mapdh9a  40660  pellex  41573  jm2.27  41747