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  4590  tfisi  4623  funprg  5308  nnsucsssuc  6550  ecopovtrn  6691  ecopovtrng  6694  addassnqg  7449  distrnqg  7454  ltsonq  7465  ltanqg  7467  ltmnqg  7468  distrnq0  7526  addassnq0  7529  mulasssrg  7825  distrsrg  7826  lttrsr  7829  ltsosr  7831  ltasrg  7837  mulextsr1lem  7847  mulextsr1  7848  axmulass  7940  axdistr  7941  dmdcanap  8749  lt2msq1  8912  ltdiv2  8914  lediv2  8918  xaddass  9944  xaddass2  9945  xlt2add  9955  modqdi  10484  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  resqrtcl  11194  bdtrilem  11404  bdtri  11405  xrbdtri  11441  bitsfzo  12119  prmexpb  12319  4sqlem18  12577  subgabl  13462  opprringbg  13636  cnptoprest  14475  ssblps  14661  ssbl  14662  plyadd  14987  plymul  14988  rplogbchbase  15186  rplogbreexp  15189  relogbcxpbap  15201  lgssq  15281