Theorem simp3ll 1246

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

Assertion

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

Proof of Theorem simp3ll

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  f1oiso2  7307  omeu  8520  ntrivcvgmul  15867  tsmsxp  24120  tgqioo  24765  ovolunlem2  25465  plyadd  26182  plymul  26183  coeeu  26190  nosupbnd1lem2  27673  noinfbnd1lem2  27688  tghilberti2  28706  btwnconn1lem2  36270  btwnconn1lem3  36271  btwnconn1lem12  36280  athgt  39902  2llnjN  40013  4atlem12b  40057  lncmp  40229  cdlema2N  40238  cdlemc2  40638  cdleme5  40686  cdleme11a  40706  cdleme21ct  40775  cdleme21  40783  cdleme22eALTN  40791  cdleme24  40798  cdleme27cl  40812  cdleme27a  40813  cdleme28  40819  cdleme36a  40906  cdleme42b  40924  cdleme48fvg  40946  cdlemf  41009  cdlemk39  41362  cdlemkid1  41368  dihlsscpre  41680  dihord4  41704  dihord5apre  41708  dihmeetlem20N  41772  mapdh9a  42235  pellex  43263  jm2.27  43436