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  4587  tfisi  4620  funprg  5305  nnsucsssuc  6547  ecopovtrn  6688  ecopovtrng  6691  addassnqg  7444  distrnqg  7449  ltsonq  7460  ltanqg  7462  ltmnqg  7463  distrnq0  7521  addassnq0  7524  mulasssrg  7820  distrsrg  7821  lttrsr  7824  ltsosr  7826  ltasrg  7832  mulextsr1lem  7842  mulextsr1  7843  axmulass  7935  axdistr  7936  dmdcanap  8743  lt2msq1  8906  ltdiv2  8908  lediv2  8912  xaddass  9938  xaddass2  9939  xlt2add  9949  modqdi  10466  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  resqrtcl  11176  bdtrilem  11385  bdtri  11386  xrbdtri  11422  prmexpb  12292  4sqlem18  12549  subgabl  13405  opprringbg  13579  cnptoprest  14418  ssblps  14604  ssbl  14605  plyadd  14930  plymul  14931  rplogbchbase  15123  rplogbreexp  15126  relogbcxpbap  15138  lgssq  15197