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  7334  addassnqg  7466  ltsonq  7482  ltanqg  7484  ltmnqg  7485  addassnq0  7546  mulasssrg  7842  distrsrg  7843  lttrsr  7846  ltsosr  7848  ltasrg  7854  mulextsr1lem  7864  mulextsr1  7865  axmulass  7957  axdistr  7958  lemul1  8637  reapmul1lem  8638  reapmul1  8639  mulcanap  8709  mulcanap2  8710  divassap  8734  divdirap  8741  div11ap  8744  muldivdirap  8751  divcanap5  8758  apmul1  8832  apmul2  8833  ltdiv1  8912  ltmuldiv  8918  ledivmul  8921  lemuldiv  8925  ltdiv2  8931  lediv2  8935  ltdiv23  8936  lediv23  8937  xaddass2  9962  xlt2add  9972  modqdi  10501  expaddzap  10692  expmulzap  10694  leisorel  10946  resqrtcl  11211  xrbdtri  11458  dvdscmulr  12002  dvdsmulcr  12003  dvdsadd2b  12022  dvdsgcd  12204  rpexp12i  12348  pythagtriplem3  12461  pcpremul  12487  pceu  12489  pcqmul  12497  pcqdiv  12501  f1ocpbllem  13012  ercpbl  13033  erlecpbl  13034  cmn4  13511  ablsub4  13519  abladdsub4  13520  lidlsubcl  14119  psmetlecl  14654  xmetlecl  14687