Theorem simp1l 1023

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

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

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 982

This theorem is referenced by:  simpl1l  1050  simpr1l  1056  simp11l  1110  simp21l  1116  simp31l  1122  en2lp  4591  tfisi  4624  funprg  5309  nnsucsssuc  6559  ecopovtrn  6700  ecopovtrng  6703  addassnqg  7468  distrnqg  7473  ltsonq  7484  ltanqg  7486  ltmnqg  7487  distrnq0  7545  addassnq0  7548  mulasssrg  7844  distrsrg  7845  lttrsr  7848  ltsosr  7850  ltasrg  7856  mulextsr1lem  7866  mulextsr1  7867  axmulass  7959  axdistr  7960  dmdcanap  8768  lt2msq1  8931  ltdiv2  8933  lediv2  8937  xaddass  9963  xaddass2  9964  xlt2add  9974  modqdi  10503  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  resqrtcl  11213  bdtrilem  11423  bdtri  11424  xrbdtri  11460  bitsfzo  12139  prmexpb  12346  4sqlem18  12604  subgabl  13540  opprringbg  13714  cnptoprest  14583  ssblps  14769  ssbl  14770  plyadd  15095  plymul  15096  rplogbchbase  15294  rplogbreexp  15297  relogbcxpbap  15309  lgssq  15389