Theorem simp3ll 1125

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

Assertion

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

Proof of Theorem simp3ll

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  f1oiso2  6502  omeu  7552  ntrivcvgmul  14473  tsmsxp  21768  tgqioo  22411  ovolunlem2  23073  plyadd  23777  plymul  23778  coeeu  23785  tghilberti2  25333  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem12  31375  athgt  33760  2llnjN  33871  4atlem12b  33915  lncmp  34087  cdlema2N  34096  cdlemc2  34497  cdleme5  34545  cdleme11a  34565  cdleme21ct  34635  cdleme21  34643  cdleme22eALTN  34651  cdleme24  34658  cdleme27cl  34672  cdleme27a  34673  cdleme28  34679  cdleme36a  34766  cdleme42b  34784  cdleme48fvg  34806  cdlemf  34869  cdlemk39  35222  cdlemkid1  35228  dihlsscpre  35541  dihord4  35565  dihord5apre  35569  dihmeetlem20N  35633  mapdh9a  36097  pellex  36417  jm2.27  36593