Theorem simp3l 1030

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

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

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 985

This theorem is referenced by:  simpl3l  1057  simpr3l  1063  simp13l  1117  simp23l  1123  simp33l  1129  issod  4387  tfisi  4656  tfrlem5  6430  tfrlemibxssdm  6443  tfr1onlembxssdm  6459  tfrcllembxssdm  6472  ecopovtrn  6749  ecopovtrng  6752  dftap2  7405  addassnqg  7537  ltsonq  7553  ltanqg  7555  ltmnqg  7556  addassnq0  7617  mulasssrg  7913  distrsrg  7914  lttrsr  7917  ltsosr  7919  ltasrg  7925  mulextsr1lem  7935  mulextsr1  7936  axmulass  8028  axdistr  8029  lemul1  8708  reapmul1lem  8709  reapmul1  8710  mulcanap  8780  mulcanap2  8781  divassap  8805  divdirap  8812  div11ap  8815  muldivdirap  8822  divcanap5  8829  apmul1  8903  apmul2  8904  ltdiv1  8983  ltmuldiv  8989  ledivmul  8992  lemuldiv  8996  ltdiv2  9002  lediv2  9006  ltdiv23  9007  lediv23  9008  xaddass2  10034  xlt2add  10044  modqdi  10581  expaddzap  10772  expmulzap  10774  leisorel  11026  resqrtcl  11506  xrbdtri  11753  dvdscmulr  12297  dvdsmulcr  12298  dvdsadd2b  12317  dvdsgcd  12499  rpexp12i  12643  pythagtriplem3  12756  pcpremul  12782  pceu  12784  pcqmul  12792  pcqdiv  12796  f1ocpbllem  13309  ercpbl  13330  erlecpbl  13331  cmn4  13808  ablsub4  13816  abladdsub4  13817  lidlsubcl  14416  psmetlecl  14973  xmetlecl  15006