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  4241  tfisi  4501  tfrlem5  6211  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  ecopovtrn  6526  ecopovtrng  6529  addassnqg  7190  ltsonq  7206  ltanqg  7208  ltmnqg  7209  addassnq0  7270  mulasssrg  7566  distrsrg  7567  lttrsr  7570  ltsosr  7572  ltasrg  7578  mulextsr1lem  7588  mulextsr1  7589  axmulass  7681  axdistr  7682  lemul1  8355  reapmul1lem  8356  reapmul1  8357  mulcanap  8426  mulcanap2  8427  divassap  8450  divdirap  8457  div11ap  8460  muldivdirap  8467  divcanap5  8474  apmul1  8548  apmul2  8549  ltdiv1  8626  ltmuldiv  8632  ledivmul  8635  lemuldiv  8639  ltdiv2  8645  lediv2  8649  ltdiv23  8650  lediv23  8651  xaddass2  9653  xlt2add  9663  modqdi  10165  expaddzap  10337  expmulzap  10339  leisorel  10580  resqrtcl  10801  xrbdtri  11045  dvdscmulr  11522  dvdsmulcr  11523  dvdsadd2b  11540  dvdsgcd  11700  rpexp12i  11833  psmetlecl  12503  xmetlecl  12536