Theorem simp1l 1048

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 1045	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

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

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 1007

This theorem is referenced by:  simpl1l  1075  simpr1l  1081  simp11l  1135  simp21l  1141  simp31l  1147  en2lp  4675  tfisi  4708  funprg  5405  nnsucsssuc  6724  ecopovtrn  6865  ecopovtrng  6868  addassnqg  7696  distrnqg  7701  ltsonq  7712  ltanqg  7714  ltmnqg  7715  distrnq0  7773  addassnq0  7776  mulasssrg  8072  distrsrg  8073  lttrsr  8076  ltsosr  8078  ltasrg  8084  mulextsr1lem  8094  mulextsr1  8095  axmulass  8187  axdistr  8188  dmdcanap  8995  lt2msq1  9158  ltdiv2  9160  lediv2  9164  xaddass  10201  xaddass2  10202  xlt2add  10212  modqdi  10753  expaddzaplem  10943  expaddzap  10944  expmulzap  10946  swrdspsleq  11355  pfxeq  11384  ccatopth2  11405  pfxccat3  11422  resqrtcl  11710  bdtrilem  11920  bdtri  11921  xrbdtri  11957  bitsfzo  12637  prmexpb  12844  4sqlem18  13102  subgabl  14041  opprringbg  14216  cnptoprest  15096  ssblps  15282  ssbl  15283  plyadd  15608  plymul  15609  rplogbchbase  15807  rplogbreexp  15810  relogbcxpbap  15822  lgssq  15905  uhgr2edg  16193  clwwlkccat  16388