Theorem simp3l 1020

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

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

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 975

This theorem is referenced by:  simpl3l  1047  simpr3l  1053  simp13l  1107  simp23l  1113  simp33l  1119  issod  4304  tfisi  4571  tfrlem5  6293  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  ecopovtrn  6610  ecopovtrng  6613  addassnqg  7344  ltsonq  7360  ltanqg  7362  ltmnqg  7363  addassnq0  7424  mulasssrg  7720  distrsrg  7721  lttrsr  7724  ltsosr  7726  ltasrg  7732  mulextsr1lem  7742  mulextsr1  7743  axmulass  7835  axdistr  7836  lemul1  8512  reapmul1lem  8513  reapmul1  8514  mulcanap  8583  mulcanap2  8584  divassap  8607  divdirap  8614  div11ap  8617  muldivdirap  8624  divcanap5  8631  apmul1  8705  apmul2  8706  ltdiv1  8784  ltmuldiv  8790  ledivmul  8793  lemuldiv  8797  ltdiv2  8803  lediv2  8807  ltdiv23  8808  lediv23  8809  xaddass2  9827  xlt2add  9837  modqdi  10348  expaddzap  10520  expmulzap  10522  leisorel  10772  resqrtcl  10993  xrbdtri  11239  dvdscmulr  11782  dvdsmulcr  11783  dvdsadd2b  11802  dvdsgcd  11967  rpexp12i  12109  pythagtriplem3  12221  pcpremul  12247  pceu  12249  pcqmul  12257  pcqdiv  12261  psmetlecl  13128  xmetlecl  13161