Theorem simp3ll 1263

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

Assertion

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

Proof of Theorem simp3ll

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1oiso2  7352  omeu  8577  ntrivcvgmul  16051  tsmsxp  24454  tgqioo  25099  ovolunlem2  25799  plyadd  26516  plymul  26517  coeeu  26524  nosupbnd1lem2  28048  noinfbnd1lem2  28063  tghilberti2  29088  btwnconn1lem2  36823  btwnconn1lem3  36824  btwnconn1lem12  36833  athgt  40481  2llnjN  40592  4atlem12b  40636  lncmp  40808  cdlema2N  40817  cdlemc2  41217  cdleme5  41265  cdleme11a  41285  cdleme21ct  41354  cdleme21  41362  cdleme22eALTN  41370  cdleme24  41377  cdleme27cl  41391  cdleme27a  41392  cdleme28  41398  cdleme36a  41485  cdleme42b  41503  cdleme48fvg  41525  cdlemf  41588  cdlemk39  41941  cdlemkid1  41947  dihlsscpre  42259  dihord4  42283  dihord5apre  42287  dihmeetlem20N  42351  mapdh9a  42814  pellex  43795  jm2.27  43968