Theorem simp3l 1051

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

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

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 1006

This theorem is referenced by:  simpl3l  1078  simpr3l  1084  simp13l  1138  simp23l  1144  simp33l  1150  issod  4418  tfisi  4687  tfrlem5  6485  tfrlemibxssdm  6498  tfr1onlembxssdm  6514  tfrcllembxssdm  6527  ecopovtrn  6806  ecopovtrng  6809  dftap2  7475  addassnqg  7607  ltsonq  7623  ltanqg  7625  ltmnqg  7626  addassnq0  7687  mulasssrg  7983  distrsrg  7984  lttrsr  7987  ltsosr  7989  ltasrg  7995  mulextsr1lem  8005  mulextsr1  8006  axmulass  8098  axdistr  8099  lemul1  8778  reapmul1lem  8779  reapmul1  8780  mulcanap  8850  mulcanap2  8851  divassap  8875  divdirap  8882  div11ap  8885  muldivdirap  8892  divcanap5  8899  apmul1  8973  apmul2  8974  ltdiv1  9053  ltmuldiv  9059  ledivmul  9062  lemuldiv  9066  ltdiv2  9072  lediv2  9076  ltdiv23  9077  lediv23  9078  xaddass2  10110  xlt2add  10120  modqdi  10660  expaddzap  10851  expmulzap  10853  leisorel  11107  resqrtcl  11612  xrbdtri  11859  dvdscmulr  12404  dvdsmulcr  12405  dvdsadd2b  12424  dvdsgcd  12606  rpexp12i  12750  pythagtriplem3  12863  pcpremul  12889  pceu  12891  pcqmul  12899  pcqdiv  12903  f1ocpbllem  13416  ercpbl  13437  erlecpbl  13438  cmn4  13915  ablsub4  13923  abladdsub4  13924  lidlsubcl  14525  psmetlecl  15087  xmetlecl  15120  wlkl1loop  16238