Theorem simp1l 939

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 106	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 936	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 101   ∧ w3a 896

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105

This theorem depends on definitions:  df-bi 114  df-3an 898

This theorem is referenced by:  simpl1l  966  simpr1l  972  simp11l  1026  simp21l  1032  simp31l  1038  en2lp  4305  tfisi  4337  funprg  4976  nnsucsssuc  6101  ecopovtrn  6233  ecopovtrng  6236  addassnqg  6537  distrnqg  6542  ltsonq  6553  ltanqg  6555  ltmnqg  6556  distrnq0  6614  addassnq0  6617  mulasssrg  6900  distrsrg  6901  lttrsr  6904  ltsosr  6906  ltasrg  6912  mulextsr1lem  6921  mulextsr1  6922  axmulass  7004  axdistr  7005  dmdcanap  7772  lt2msq1  7925  ltdiv2  7927  lediv2  7931  modqdi  9336  expaddzaplem  9457  expaddzap  9458  expmulzap  9460  resqrtcl  9848