Theorem simp3l 1015

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

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

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 970

This theorem is referenced by:  simpl3l  1042  simpr3l  1048  simp13l  1102  simp23l  1108  simp33l  1114  issod  4296  tfisi  4563  tfrlem5  6278  tfrlemibxssdm  6291  tfr1onlembxssdm  6307  tfrcllembxssdm  6320  ecopovtrn  6594  ecopovtrng  6597  addassnqg  7319  ltsonq  7335  ltanqg  7337  ltmnqg  7338  addassnq0  7399  mulasssrg  7695  distrsrg  7696  lttrsr  7699  ltsosr  7701  ltasrg  7707  mulextsr1lem  7717  mulextsr1  7718  axmulass  7810  axdistr  7811  lemul1  8487  reapmul1lem  8488  reapmul1  8489  mulcanap  8558  mulcanap2  8559  divassap  8582  divdirap  8589  div11ap  8592  muldivdirap  8599  divcanap5  8606  apmul1  8680  apmul2  8681  ltdiv1  8759  ltmuldiv  8765  ledivmul  8768  lemuldiv  8772  ltdiv2  8778  lediv2  8782  ltdiv23  8783  lediv23  8784  xaddass2  9802  xlt2add  9812  modqdi  10323  expaddzap  10495  expmulzap  10497  leisorel  10746  resqrtcl  10967  xrbdtri  11213  dvdscmulr  11756  dvdsmulcr  11757  dvdsadd2b  11776  dvdsgcd  11941  rpexp12i  12083  pythagtriplem3  12195  pcpremul  12221  pceu  12223  pcqmul  12231  pcqdiv  12235  psmetlecl  12934  xmetlecl  12967