Theorem simp1l 1045

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1l	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1042	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simpl1l  1072  simpr1l  1078  simp11l  1132  simp21l  1138  simp31l  1144  en2lp  4646  tfisi  4679  funprg  5371  nnsucsssuc  6646  ecopovtrn  6787  ecopovtrng  6790  addassnqg  7577  distrnqg  7582  ltsonq  7593  ltanqg  7595  ltmnqg  7596  distrnq0  7654  addassnq0  7657  mulasssrg  7953  distrsrg  7954  lttrsr  7957  ltsosr  7959  ltasrg  7965  mulextsr1lem  7975  mulextsr1  7976  axmulass  8068  axdistr  8069  dmdcanap  8877  lt2msq1  9040  ltdiv2  9042  lediv2  9046  xaddass  10073  xaddass2  10074  xlt2add  10084  modqdi  10622  expaddzaplem  10812  expaddzap  10813  expmulzap  10815  swrdspsleq  11207  pfxeq  11236  ccatopth2  11257  pfxccat3  11274  resqrtcl  11548  bdtrilem  11758  bdtri  11759  xrbdtri  11795  bitsfzo  12474  prmexpb  12681  4sqlem18  12939  subgabl  13877  opprringbg  14051  cnptoprest  14921  ssblps  15107  ssbl  15108  plyadd  15433  plymul  15434  rplogbchbase  15632  rplogbreexp  15635  relogbcxpbap  15647  lgssq  15727  uhgr2edg  16012