Theorem simp3l 1052

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

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

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 1007

This theorem is referenced by:  simpl3l  1079  simpr3l  1085  simp13l  1139  simp23l  1145  simp33l  1151  issod  4445  tfisi  4714  tfrlem5  6558  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  ecopovtrn  6879  ecopovtrng  6882  dftap2  7581  addassnqg  7713  ltsonq  7729  ltanqg  7731  ltmnqg  7732  addassnq0  7793  mulasssrg  8089  distrsrg  8090  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1lem  8111  mulextsr1  8112  axmulass  8204  axdistr  8205  lemul1  8885  reapmul1lem  8886  reapmul1  8887  mulcanap  8957  mulcanap2  8958  divassap  8984  divdirap  8991  div11ap  8994  muldivdirap  9001  divcanap5  9008  apmul1  9082  apmul2  9083  ltdiv1  9162  ltmuldiv  9168  ledivmul  9171  lemuldiv  9175  ltdiv2  9181  lediv2  9185  ltdiv23  9186  lediv23  9187  xaddass2  10225  xlt2add  10235  modqdi  10781  expaddzap  10972  expmulzap  10974  leisorel  11237  resqrtcl  11742  xrbdtri  11989  dvdscmulr  12534  dvdsmulcr  12535  dvdsadd2b  12554  dvdsgcd  12736  rpexp12i  12880  pythagtriplem3  12993  pcpremul  13019  pceu  13021  pcqmul  13029  pcqdiv  13033  f1ocpbllem  13577  ercpbl  13598  erlecpbl  13599  cmn4  14061  ablsub4  14069  abladdsub4  14070  lidlsubcl  14764  psmetlecl  15328  xmetlecl  15361  wlkl1loop  16482