Theorem simp3l 990

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

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

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

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

This theorem is referenced by:  simpl3l  1017  simpr3l  1023  simp13l  1077  simp23l  1083  simp33l  1089  issod  4199  tfisi  4459  tfrlem5  6162  tfrlemibxssdm  6175  tfr1onlembxssdm  6191  tfrcllembxssdm  6204  ecopovtrn  6477  ecopovtrng  6480  addassnqg  7131  ltsonq  7147  ltanqg  7149  ltmnqg  7150  addassnq0  7211  mulasssrg  7494  distrsrg  7495  lttrsr  7498  ltsosr  7500  ltasrg  7506  mulextsr1lem  7515  mulextsr1  7516  axmulass  7601  axdistr  7602  lemul1  8266  reapmul1lem  8267  reapmul1  8268  mulcanap  8332  mulcanap2  8333  divassap  8356  divdirap  8363  div11ap  8366  muldivdirap  8373  divcanap5  8380  apmul1  8454  apmul2  8455  ltdiv1  8529  ltmuldiv  8535  ledivmul  8538  lemuldiv  8542  ltdiv2  8548  lediv2  8552  ltdiv23  8553  lediv23  8554  xaddass2  9539  xlt2add  9549  modqdi  10051  expaddzap  10223  expmulzap  10225  leisorel  10466  resqrtcl  10686  xrbdtri  10930  dvdscmulr  11363  dvdsmulcr  11364  dvdsadd2b  11381  dvdsgcd  11539  rpexp12i  11672  psmetlecl  12316  xmetlecl  12349