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 1135	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:  f1oiso2  7298  omeu  8512  ntrivcvgmul  15825  tsmsxp  24099  tgqioo  24744  ovolunlem2  25455  plyadd  26178  plymul  26179  coeeu  26186  nosupbnd1lem2  27677  noinfbnd1lem2  27692  tghilberti2  28710  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem12  36292  athgt  39712  2llnjN  39823  4atlem12b  39867  lncmp  40039  cdlema2N  40048  cdlemc2  40448  cdleme5  40496  cdleme11a  40516  cdleme21ct  40585  cdleme21  40593  cdleme22eALTN  40601  cdleme24  40608  cdleme27cl  40622  cdleme27a  40623  cdleme28  40629  cdleme36a  40716  cdleme42b  40734  cdleme48fvg  40756  cdlemf  40819  cdlemk39  41172  cdlemkid1  41178  dihlsscpre  41490  dihord4  41514  dihord5apre  41518  dihmeetlem20N  41582  mapdh9a  42045  pellex  43073  jm2.27  43246