Theorem simp3l 1027

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpl3l  1054  simpr3l  1060  simp13l  1114  simp23l  1120  simp33l  1126  issod  4350  tfisi  4619  tfrlem5  6367  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  ecopovtrn  6686  ecopovtrng  6689  dftap2  7311  addassnqg  7442  ltsonq  7458  ltanqg  7460  ltmnqg  7461  addassnq0  7522  mulasssrg  7818  distrsrg  7819  lttrsr  7822  ltsosr  7824  ltasrg  7830  mulextsr1lem  7840  mulextsr1  7841  axmulass  7933  axdistr  7934  lemul1  8612  reapmul1lem  8613  reapmul1  8614  mulcanap  8684  mulcanap2  8685  divassap  8709  divdirap  8716  div11ap  8719  muldivdirap  8726  divcanap5  8733  apmul1  8807  apmul2  8808  ltdiv1  8887  ltmuldiv  8893  ledivmul  8896  lemuldiv  8900  ltdiv2  8906  lediv2  8910  ltdiv23  8911  lediv23  8912  xaddass2  9936  xlt2add  9946  modqdi  10463  expaddzap  10654  expmulzap  10656  leisorel  10908  resqrtcl  11173  xrbdtri  11419  dvdscmulr  11963  dvdsmulcr  11964  dvdsadd2b  11983  dvdsgcd  12149  rpexp12i  12293  pythagtriplem3  12405  pcpremul  12431  pceu  12433  pcqmul  12441  pcqdiv  12445  f1ocpbllem  12893  ercpbl  12914  erlecpbl  12915  cmn4  13375  ablsub4  13383  abladdsub4  13384  lidlsubcl  13983  psmetlecl  14502  xmetlecl  14535