Theorem simp3l 1051

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

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

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 1006

This theorem is referenced by:  simpl3l  1078  simpr3l  1084  simp13l  1138  simp23l  1144  simp33l  1150  issod  4416  tfisi  4685  tfrlem5  6480  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  ecopovtrn  6801  ecopovtrng  6804  dftap2  7470  addassnqg  7602  ltsonq  7618  ltanqg  7620  ltmnqg  7621  addassnq0  7682  mulasssrg  7978  distrsrg  7979  lttrsr  7982  ltsosr  7984  ltasrg  7990  mulextsr1lem  8000  mulextsr1  8001  axmulass  8093  axdistr  8094  lemul1  8773  reapmul1lem  8774  reapmul1  8775  mulcanap  8845  mulcanap2  8846  divassap  8870  divdirap  8877  div11ap  8880  muldivdirap  8887  divcanap5  8894  apmul1  8968  apmul2  8969  ltdiv1  9048  ltmuldiv  9054  ledivmul  9057  lemuldiv  9061  ltdiv2  9067  lediv2  9071  ltdiv23  9072  lediv23  9073  xaddass2  10105  xlt2add  10115  modqdi  10655  expaddzap  10846  expmulzap  10848  leisorel  11102  resqrtcl  11591  xrbdtri  11838  dvdscmulr  12383  dvdsmulcr  12384  dvdsadd2b  12403  dvdsgcd  12585  rpexp12i  12729  pythagtriplem3  12842  pcpremul  12868  pceu  12870  pcqmul  12878  pcqdiv  12882  f1ocpbllem  13395  ercpbl  13416  erlecpbl  13417  cmn4  13894  ablsub4  13902  abladdsub4  13903  lidlsubcl  14504  psmetlecl  15061  xmetlecl  15094  wlkl1loop  16212