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  4442  tfisi  4711  tfrlem5  6547  tfrlemibxssdm  6560  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  ecopovtrn  6868  ecopovtrng  6871  dftap2  7570  addassnqg  7702  ltsonq  7718  ltanqg  7720  ltmnqg  7721  addassnq0  7782  mulasssrg  8078  distrsrg  8079  lttrsr  8082  ltsosr  8084  ltasrg  8090  mulextsr1lem  8100  mulextsr1  8101  axmulass  8193  axdistr  8194  lemul1  8872  reapmul1lem  8873  reapmul1  8874  mulcanap  8944  mulcanap2  8945  divassap  8969  divdirap  8976  div11ap  8979  muldivdirap  8986  divcanap5  8993  apmul1  9067  apmul2  9068  ltdiv1  9147  ltmuldiv  9153  ledivmul  9156  lemuldiv  9160  ltdiv2  9166  lediv2  9170  ltdiv23  9171  lediv23  9172  xaddass2  10209  xlt2add  10219  modqdi  10761  expaddzap  10952  expmulzap  10954  leisorel  11217  resqrtcl  11722  xrbdtri  11969  dvdscmulr  12514  dvdsmulcr  12515  dvdsadd2b  12534  dvdsgcd  12716  rpexp12i  12860  pythagtriplem3  12973  pcpremul  12999  pceu  13001  pcqmul  13009  pcqdiv  13013  f1ocpbllem  13544  ercpbl  13565  erlecpbl  13566  cmn4  14043  ablsub4  14051  abladdsub4  14052  lidlsubcl  14684  psmetlecl  15248  xmetlecl  15281  wlkl1loop  16402