Theorem simp3l 1010

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

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

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 965

This theorem is referenced by:  simpl3l  1037  simpr3l  1043  simp13l  1097  simp23l  1103  simp33l  1109  issod  4274  tfisi  4540  tfrlem5  6251  tfrlemibxssdm  6264  tfr1onlembxssdm  6280  tfrcllembxssdm  6293  ecopovtrn  6566  ecopovtrng  6569  addassnqg  7281  ltsonq  7297  ltanqg  7299  ltmnqg  7300  addassnq0  7361  mulasssrg  7657  distrsrg  7658  lttrsr  7661  ltsosr  7663  ltasrg  7669  mulextsr1lem  7679  mulextsr1  7680  axmulass  7772  axdistr  7773  lemul1  8447  reapmul1lem  8448  reapmul1  8449  mulcanap  8518  mulcanap2  8519  divassap  8542  divdirap  8549  div11ap  8552  muldivdirap  8559  divcanap5  8566  apmul1  8640  apmul2  8641  ltdiv1  8718  ltmuldiv  8724  ledivmul  8727  lemuldiv  8731  ltdiv2  8737  lediv2  8741  ltdiv23  8742  lediv23  8743  xaddass2  9752  xlt2add  9762  modqdi  10269  expaddzap  10441  expmulzap  10443  leisorel  10685  resqrtcl  10906  xrbdtri  11150  dvdscmulr  11689  dvdsmulcr  11690  dvdsadd2b  11707  dvdsgcd  11868  rpexp12i  12001  psmetlecl  12681  xmetlecl  12714