Theorem simp3l 1028

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

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

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 983

This theorem is referenced by:  simpl3l  1055  simpr3l  1061  simp13l  1115  simp23l  1121  simp33l  1127  issod  4370  tfisi  4639  tfrlem5  6407  tfrlemibxssdm  6420  tfr1onlembxssdm  6436  tfrcllembxssdm  6449  ecopovtrn  6726  ecopovtrng  6729  dftap2  7370  addassnqg  7502  ltsonq  7518  ltanqg  7520  ltmnqg  7521  addassnq0  7582  mulasssrg  7878  distrsrg  7879  lttrsr  7882  ltsosr  7884  ltasrg  7890  mulextsr1lem  7900  mulextsr1  7901  axmulass  7993  axdistr  7994  lemul1  8673  reapmul1lem  8674  reapmul1  8675  mulcanap  8745  mulcanap2  8746  divassap  8770  divdirap  8777  div11ap  8780  muldivdirap  8787  divcanap5  8794  apmul1  8868  apmul2  8869  ltdiv1  8948  ltmuldiv  8954  ledivmul  8957  lemuldiv  8961  ltdiv2  8967  lediv2  8971  ltdiv23  8972  lediv23  8973  xaddass2  9999  xlt2add  10009  modqdi  10544  expaddzap  10735  expmulzap  10737  leisorel  10989  resqrtcl  11384  xrbdtri  11631  dvdscmulr  12175  dvdsmulcr  12176  dvdsadd2b  12195  dvdsgcd  12377  rpexp12i  12521  pythagtriplem3  12634  pcpremul  12660  pceu  12662  pcqmul  12670  pcqdiv  12674  f1ocpbllem  13186  ercpbl  13207  erlecpbl  13208  cmn4  13685  ablsub4  13693  abladdsub4  13694  lidlsubcl  14293  psmetlecl  14850  xmetlecl  14883