Theorem simp3l 1027

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

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

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 982

This theorem is referenced by:  simpl3l  1054  simpr3l  1060  simp13l  1114  simp23l  1120  simp33l  1126  issod  4351  tfisi  4620  tfrlem5  6369  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  ecopovtrn  6688  ecopovtrng  6691  dftap2  7313  addassnqg  7444  ltsonq  7460  ltanqg  7462  ltmnqg  7463  addassnq0  7524  mulasssrg  7820  distrsrg  7821  lttrsr  7824  ltsosr  7826  ltasrg  7832  mulextsr1lem  7842  mulextsr1  7843  axmulass  7935  axdistr  7936  lemul1  8614  reapmul1lem  8615  reapmul1  8616  mulcanap  8686  mulcanap2  8687  divassap  8711  divdirap  8718  div11ap  8721  muldivdirap  8728  divcanap5  8735  apmul1  8809  apmul2  8810  ltdiv1  8889  ltmuldiv  8895  ledivmul  8898  lemuldiv  8902  ltdiv2  8908  lediv2  8912  ltdiv23  8913  lediv23  8914  xaddass2  9939  xlt2add  9949  modqdi  10466  expaddzap  10657  expmulzap  10659  leisorel  10911  resqrtcl  11176  xrbdtri  11422  dvdscmulr  11966  dvdsmulcr  11967  dvdsadd2b  11986  dvdsgcd  12152  rpexp12i  12296  pythagtriplem3  12408  pcpremul  12434  pceu  12436  pcqmul  12444  pcqdiv  12448  f1ocpbllem  12896  ercpbl  12917  erlecpbl  12918  cmn4  13378  ablsub4  13386  abladdsub4  13387  lidlsubcl  13986  psmetlecl  14513  xmetlecl  14546