Theorem simp3l 1049

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

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

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 1004

This theorem is referenced by:  simpl3l  1076  simpr3l  1082  simp13l  1136  simp23l  1142  simp33l  1148  issod  4411  tfisi  4680  tfrlem5  6471  tfrlemibxssdm  6484  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  ecopovtrn  6792  ecopovtrng  6795  dftap2  7453  addassnqg  7585  ltsonq  7601  ltanqg  7603  ltmnqg  7604  addassnq0  7665  mulasssrg  7961  distrsrg  7962  lttrsr  7965  ltsosr  7967  ltasrg  7973  mulextsr1lem  7983  mulextsr1  7984  axmulass  8076  axdistr  8077  lemul1  8756  reapmul1lem  8757  reapmul1  8758  mulcanap  8828  mulcanap2  8829  divassap  8853  divdirap  8860  div11ap  8863  muldivdirap  8870  divcanap5  8877  apmul1  8951  apmul2  8952  ltdiv1  9031  ltmuldiv  9037  ledivmul  9040  lemuldiv  9044  ltdiv2  9050  lediv2  9054  ltdiv23  9055  lediv23  9056  xaddass2  10083  xlt2add  10093  modqdi  10631  expaddzap  10822  expmulzap  10824  leisorel  11077  resqrtcl  11561  xrbdtri  11808  dvdscmulr  12352  dvdsmulcr  12353  dvdsadd2b  12372  dvdsgcd  12554  rpexp12i  12698  pythagtriplem3  12811  pcpremul  12837  pceu  12839  pcqmul  12847  pcqdiv  12851  f1ocpbllem  13364  ercpbl  13385  erlecpbl  13386  cmn4  13863  ablsub4  13871  abladdsub4  13872  lidlsubcl  14472  psmetlecl  15029  xmetlecl  15062  wlkl1loop  16130