Theorem simp3l 1056

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl3l  1083  simpr3l  1089  simp13l  1143  simp23l  1149  simp33l  1155  issod  4466  tfisi  4736  tfrlem5  6589  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  ecopovtrn  6910  ecopovtrng  6913  dftap2  7624  addassnqg  7756  ltsonq  7772  ltanqg  7774  ltmnqg  7775  addassnq0  7836  mulasssrg  8132  distrsrg  8133  lttrsr  8136  ltsosr  8138  ltasrg  8144  mulextsr1lem  8154  mulextsr1  8155  axmulass  8247  axdistr  8248  lemul1  8930  reapmul1lem  8931  reapmul1  8932  mulcanap  9002  mulcanap2  9003  divassap  9029  divdirap  9036  div11ap  9039  muldivdirap  9046  divcanap5  9053  apmul1  9127  apmul2  9128  ltdiv1  9207  ltmuldiv  9213  ledivmul  9216  lemuldiv  9220  ltdiv2  9226  lediv2  9230  ltdiv23  9231  lediv23  9232  xaddass2  10290  xlt2add  10300  modqdi  10851  expaddzap  11042  expmulzap  11044  leisorel  11312  resqrtcl  11818  xrbdtri  12068  dvdscmulr  12613  dvdsmulcr  12614  dvdsadd2b  12633  dvdsgcd  12815  rpexp12i  12960  pythagtriplem3  13076  pcpremul  13102  pceu  13104  pcqmul  13112  pcqdiv  13116  f1ocpbllem  13691  ercpbl  13712  erlecpbl  13713  cmn4  14199  ablsub4  14208  abladdsub4  14209  lidlsubcl  14934  psmetlecl  15572  xmetlecl  15605  wlkl1loop  16816