Theorem simp3l 1025

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

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

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 980

This theorem is referenced by:  simpl3l  1052  simpr3l  1058  simp13l  1112  simp23l  1118  simp33l  1124  issod  4319  tfisi  4586  tfrlem5  6314  tfrlemibxssdm  6327  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  ecopovtrn  6631  ecopovtrng  6634  dftap2  7249  addassnqg  7380  ltsonq  7396  ltanqg  7398  ltmnqg  7399  addassnq0  7460  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1lem  7778  mulextsr1  7779  axmulass  7871  axdistr  7872  lemul1  8548  reapmul1lem  8549  reapmul1  8550  mulcanap  8620  mulcanap2  8621  divassap  8645  divdirap  8652  div11ap  8655  muldivdirap  8662  divcanap5  8669  apmul1  8743  apmul2  8744  ltdiv1  8823  ltmuldiv  8829  ledivmul  8832  lemuldiv  8836  ltdiv2  8842  lediv2  8846  ltdiv23  8847  lediv23  8848  xaddass2  9868  xlt2add  9878  modqdi  10389  expaddzap  10561  expmulzap  10563  leisorel  10812  resqrtcl  11033  xrbdtri  11279  dvdscmulr  11822  dvdsmulcr  11823  dvdsadd2b  11842  dvdsgcd  12007  rpexp12i  12149  pythagtriplem3  12261  pcpremul  12287  pceu  12289  pcqmul  12297  pcqdiv  12301  f1ocpbllem  12713  cmn4  13061  ablsub4  13069  abladdsub4  13070  psmetlecl  13727  xmetlecl  13760