Theorem simp3l 966

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 107	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 961	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpl3l  993  simpr3l  999  simp13l  1053  simp23l  1059  simp33l  1065  issod  4074  tfisi  4328  tfrlem5  5953  tfrlemibxssdm  5964  ecopovtrn  6226  ecopovtrng  6229  addassnqg  6572  ltsonq  6588  ltanqg  6590  ltmnqg  6591  addassnq0  6652  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltsosr  6941  ltasrg  6947  mulextsr1lem  6956  mulextsr1  6957  axmulass  7039  axdistr  7040  lemul1  7693  reapmul1lem  7694  reapmul1  7695  mulcanap  7755  mulcanap2  7756  divassap  7778  divdirap  7785  div11ap  7788  muldivdirap  7795  divcanap5  7802  apmul1  7876  ltdiv1  7946  ltmuldiv  7952  ledivmul  7955  lemuldiv  7959  ltdiv2  7965  lediv2  7969  ltdiv23  7970  lediv23  7971  modqdi  9394  expaddzap  9520  expmulzap  9522  resqrtcl  9915  dvdscmulr  10224  dvdsmulcr  10225  dvdsadd2b  10242  dvdsgcd  10401  rpexp12i  10534