Theorem simp3l 1049

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

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

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 1004

This theorem is referenced by:  simpl3l  1076  simpr3l  1082  simp13l  1136  simp23l  1142  simp33l  1148  issod  4414  tfisi  4683  tfrlem5  6475  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  ecopovtrn  6796  ecopovtrng  6799  dftap2  7463  addassnqg  7595  ltsonq  7611  ltanqg  7613  ltmnqg  7614  addassnq0  7675  mulasssrg  7971  distrsrg  7972  lttrsr  7975  ltsosr  7977  ltasrg  7983  mulextsr1lem  7993  mulextsr1  7994  axmulass  8086  axdistr  8087  lemul1  8766  reapmul1lem  8767  reapmul1  8768  mulcanap  8838  mulcanap2  8839  divassap  8863  divdirap  8870  div11ap  8873  muldivdirap  8880  divcanap5  8887  apmul1  8961  apmul2  8962  ltdiv1  9041  ltmuldiv  9047  ledivmul  9050  lemuldiv  9054  ltdiv2  9060  lediv2  9064  ltdiv23  9065  lediv23  9066  xaddass2  10098  xlt2add  10108  modqdi  10647  expaddzap  10838  expmulzap  10840  leisorel  11094  resqrtcl  11583  xrbdtri  11830  dvdscmulr  12374  dvdsmulcr  12375  dvdsadd2b  12394  dvdsgcd  12576  rpexp12i  12720  pythagtriplem3  12833  pcpremul  12859  pceu  12861  pcqmul  12869  pcqdiv  12873  f1ocpbllem  13386  ercpbl  13407  erlecpbl  13408  cmn4  13885  ablsub4  13893  abladdsub4  13894  lidlsubcl  14494  psmetlecl  15051  xmetlecl  15084  wlkl1loop  16169