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  4439  tfisi  4708  tfrlem5  6544  tfrlemibxssdm  6557  tfr1onlembxssdm  6573  tfrcllembxssdm  6586  ecopovtrn  6865  ecopovtrng  6868  dftap2  7561  addassnqg  7693  ltsonq  7709  ltanqg  7711  ltmnqg  7712  addassnq0  7773  mulasssrg  8069  distrsrg  8070  lttrsr  8073  ltsosr  8075  ltasrg  8081  mulextsr1lem  8091  mulextsr1  8092  axmulass  8184  axdistr  8185  lemul1  8863  reapmul1lem  8864  reapmul1  8865  mulcanap  8935  mulcanap2  8936  divassap  8960  divdirap  8967  div11ap  8970  muldivdirap  8977  divcanap5  8984  apmul1  9058  apmul2  9059  ltdiv1  9138  ltmuldiv  9144  ledivmul  9147  lemuldiv  9151  ltdiv2  9157  lediv2  9161  ltdiv23  9162  lediv23  9163  xaddass2  10199  xlt2add  10209  modqdi  10750  expaddzap  10941  expmulzap  10943  leisorel  11202  resqrtcl  11707  xrbdtri  11954  dvdscmulr  12499  dvdsmulcr  12500  dvdsadd2b  12519  dvdsgcd  12701  rpexp12i  12845  pythagtriplem3  12958  pcpremul  12984  pceu  12986  pcqmul  12994  pcqdiv  12998  f1ocpbllem  13512  ercpbl  13533  erlecpbl  13534  cmn4  14011  ablsub4  14019  abladdsub4  14020  lidlsubcl  14622  psmetlecl  15186  xmetlecl  15219  wlkl1loop  16340