Theorem simp3l 1009

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp3l	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 108	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1004	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simpl3l  1036  simpr3l  1042  simp13l  1096  simp23l  1102  simp33l  1108  issod  4236  tfisi  4496  tfrlem5  6204  tfrlemibxssdm  6217  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  ecopovtrn  6519  ecopovtrng  6522  addassnqg  7183  ltsonq  7199  ltanqg  7201  ltmnqg  7202  addassnq0  7263  mulasssrg  7559  distrsrg  7560  lttrsr  7563  ltsosr  7565  ltasrg  7571  mulextsr1lem  7581  mulextsr1  7582  axmulass  7674  axdistr  7675  lemul1  8348  reapmul1lem  8349  reapmul1  8350  mulcanap  8419  mulcanap2  8420  divassap  8443  divdirap  8450  div11ap  8453  muldivdirap  8460  divcanap5  8467  apmul1  8541  apmul2  8542  ltdiv1  8619  ltmuldiv  8625  ledivmul  8628  lemuldiv  8632  ltdiv2  8638  lediv2  8642  ltdiv23  8643  lediv23  8644  xaddass2  9646  xlt2add  9656  modqdi  10158  expaddzap  10330  expmulzap  10332  leisorel  10573  resqrtcl  10794  xrbdtri  11038  dvdscmulr  11511  dvdsmulcr  11512  dvdsadd2b  11529  dvdsgcd  11689  rpexp12i  11822  psmetlecl  12492  xmetlecl  12525