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  4643  tfisi  4676  funprg  5367  nnsucsssuc  6628  ecopovtrn  6769  ecopovtrng  6772  addassnqg  7557  distrnqg  7562  ltsonq  7573  ltanqg  7575  ltmnqg  7576  distrnq0  7634  addassnq0  7637  mulasssrg  7933  distrsrg  7934  lttrsr  7937  ltsosr  7939  ltasrg  7945  mulextsr1lem  7955  mulextsr1  7956  axmulass  8048  axdistr  8049  dmdcanap  8857  lt2msq1  9020  ltdiv2  9022  lediv2  9026  xaddass  10053  xaddass2  10054  xlt2add  10064  modqdi  10601  expaddzaplem  10791  expaddzap  10792  expmulzap  10794  swrdspsleq  11185  pfxeq  11214  ccatopth2  11235  pfxccat3  11252  resqrtcl  11526  bdtrilem  11736  bdtri  11737  xrbdtri  11773  bitsfzo  12452  prmexpb  12659  4sqlem18  12917  subgabl  13855  opprringbg  14029  cnptoprest  14898  ssblps  15084  ssbl  15085  plyadd  15410  plymul  15411  rplogbchbase  15609  rplogbreexp  15612  relogbcxpbap  15624  lgssq  15704  uhgr2edg  15989