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  4650  tfisi  4683  funprg  5377  nnsucsssuc  6655  ecopovtrn  6796  ecopovtrng  6799  addassnqg  7595  distrnqg  7600  ltsonq  7611  ltanqg  7613  ltmnqg  7614  distrnq0  7672  addassnq0  7675  mulasssrg  7971  distrsrg  7972  lttrsr  7975  ltsosr  7977  ltasrg  7983  mulextsr1lem  7993  mulextsr1  7994  axmulass  8086  axdistr  8087  dmdcanap  8895  lt2msq1  9058  ltdiv2  9060  lediv2  9064  xaddass  10097  xaddass2  10098  xlt2add  10108  modqdi  10647  expaddzaplem  10837  expaddzap  10838  expmulzap  10840  swrdspsleq  11241  pfxeq  11270  ccatopth2  11291  pfxccat3  11308  resqrtcl  11583  bdtrilem  11793  bdtri  11794  xrbdtri  11830  bitsfzo  12509  prmexpb  12716  4sqlem18  12974  subgabl  13912  opprringbg  14086  cnptoprest  14956  ssblps  15142  ssbl  15143  plyadd  15468  plymul  15469  rplogbchbase  15667  rplogbreexp  15670  relogbcxpbap  15682  lgssq  15762  uhgr2edg  16050  clwwlkccat  16210