Theorem simp1l 1024

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

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

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 983

This theorem is referenced by:  simpl1l  1051  simpr1l  1057  simp11l  1111  simp21l  1117  simp31l  1123  en2lp  4607  tfisi  4640  funprg  5330  nnsucsssuc  6588  ecopovtrn  6729  ecopovtrng  6732  addassnqg  7508  distrnqg  7513  ltsonq  7524  ltanqg  7526  ltmnqg  7527  distrnq0  7585  addassnq0  7588  mulasssrg  7884  distrsrg  7885  lttrsr  7888  ltsosr  7890  ltasrg  7896  mulextsr1lem  7906  mulextsr1  7907  axmulass  7999  axdistr  8000  dmdcanap  8808  lt2msq1  8971  ltdiv2  8973  lediv2  8977  xaddass  10004  xaddass2  10005  xlt2add  10015  modqdi  10550  expaddzaplem  10740  expaddzap  10741  expmulzap  10743  swrdspsleq  11134  pfxeq  11161  resqrtcl  11390  bdtrilem  11600  bdtri  11601  xrbdtri  11637  bitsfzo  12316  prmexpb  12523  4sqlem18  12781  subgabl  13718  opprringbg  13892  cnptoprest  14761  ssblps  14947  ssbl  14948  plyadd  15273  plymul  15274  rplogbchbase  15472  rplogbreexp  15475  relogbcxpbap  15487  lgssq  15567