Theorem simp3l 1025

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

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

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 980

This theorem is referenced by:  simpl3l  1052  simpr3l  1058  simp13l  1112  simp23l  1118  simp33l  1124  issod  4321  tfisi  4588  tfrlem5  6317  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  ecopovtrn  6634  ecopovtrng  6637  dftap2  7252  addassnqg  7383  ltsonq  7399  ltanqg  7401  ltmnqg  7402  addassnq0  7463  mulasssrg  7759  distrsrg  7760  lttrsr  7763  ltsosr  7765  ltasrg  7771  mulextsr1lem  7781  mulextsr1  7782  axmulass  7874  axdistr  7875  lemul1  8552  reapmul1lem  8553  reapmul1  8554  mulcanap  8624  mulcanap2  8625  divassap  8649  divdirap  8656  div11ap  8659  muldivdirap  8666  divcanap5  8673  apmul1  8747  apmul2  8748  ltdiv1  8827  ltmuldiv  8833  ledivmul  8836  lemuldiv  8840  ltdiv2  8846  lediv2  8850  ltdiv23  8851  lediv23  8852  xaddass2  9872  xlt2add  9882  modqdi  10394  expaddzap  10566  expmulzap  10568  leisorel  10819  resqrtcl  11040  xrbdtri  11286  dvdscmulr  11829  dvdsmulcr  11830  dvdsadd2b  11849  dvdsgcd  12015  rpexp12i  12157  pythagtriplem3  12269  pcpremul  12295  pceu  12297  pcqmul  12305  pcqdiv  12309  f1ocpbllem  12736  ercpbl  12755  erlecpbl  12756  cmn4  13113  ablsub4  13121  abladdsub4  13122  psmetlecl  13873  xmetlecl  13906