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  4355  tfisi  4624  tfrlem5  6381  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  ecopovtrn  6700  ecopovtrng  6703  dftap2  7336  addassnqg  7468  ltsonq  7484  ltanqg  7486  ltmnqg  7487  addassnq0  7548  mulasssrg  7844  distrsrg  7845  lttrsr  7848  ltsosr  7850  ltasrg  7856  mulextsr1lem  7866  mulextsr1  7867  axmulass  7959  axdistr  7960  lemul1  8639  reapmul1lem  8640  reapmul1  8641  mulcanap  8711  mulcanap2  8712  divassap  8736  divdirap  8743  div11ap  8746  muldivdirap  8753  divcanap5  8760  apmul1  8834  apmul2  8835  ltdiv1  8914  ltmuldiv  8920  ledivmul  8923  lemuldiv  8927  ltdiv2  8933  lediv2  8937  ltdiv23  8938  lediv23  8939  xaddass2  9964  xlt2add  9974  modqdi  10503  expaddzap  10694  expmulzap  10696  leisorel  10948  resqrtcl  11213  xrbdtri  11460  dvdscmulr  12004  dvdsmulcr  12005  dvdsadd2b  12024  dvdsgcd  12206  rpexp12i  12350  pythagtriplem3  12463  pcpremul  12489  pceu  12491  pcqmul  12499  pcqdiv  12503  f1ocpbllem  13014  ercpbl  13035  erlecpbl  13036  cmn4  13513  ablsub4  13521  abladdsub4  13522  lidlsubcl  14121  psmetlecl  14656  xmetlecl  14689