Theorem simp3l 1049

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

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

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 1004

This theorem is referenced by:  simpl3l  1076  simpr3l  1082  simp13l  1136  simp23l  1142  simp33l  1148  issod  4410  tfisi  4679  tfrlem5  6466  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  ecopovtrn  6787  ecopovtrng  6790  dftap2  7445  addassnqg  7577  ltsonq  7593  ltanqg  7595  ltmnqg  7596  addassnq0  7657  mulasssrg  7953  distrsrg  7954  lttrsr  7957  ltsosr  7959  ltasrg  7965  mulextsr1lem  7975  mulextsr1  7976  axmulass  8068  axdistr  8069  lemul1  8748  reapmul1lem  8749  reapmul1  8750  mulcanap  8820  mulcanap2  8821  divassap  8845  divdirap  8852  div11ap  8855  muldivdirap  8862  divcanap5  8869  apmul1  8943  apmul2  8944  ltdiv1  9023  ltmuldiv  9029  ledivmul  9032  lemuldiv  9036  ltdiv2  9042  lediv2  9046  ltdiv23  9047  lediv23  9048  xaddass2  10074  xlt2add  10084  modqdi  10622  expaddzap  10813  expmulzap  10815  leisorel  11067  resqrtcl  11548  xrbdtri  11795  dvdscmulr  12339  dvdsmulcr  12340  dvdsadd2b  12359  dvdsgcd  12541  rpexp12i  12685  pythagtriplem3  12798  pcpremul  12824  pceu  12826  pcqmul  12834  pcqdiv  12838  f1ocpbllem  13351  ercpbl  13372  erlecpbl  13373  cmn4  13850  ablsub4  13858  abladdsub4  13859  lidlsubcl  14459  psmetlecl  15016  xmetlecl  15049  wlkl1loop  16079