Theorem simpl3 944

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl3	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simp3 941	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	adantr 270	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  simpll3  980  simprl3  986  simp1l3  1034  simp2l3  1040  simp3l3  1046  3anandirs  1280  frirrg  4107  fcofo  5449  acexmid  5536  rdgon  6029  oawordi  6107  nnmord  6149  nnmword  6150  fidifsnen  6395  dif1en  6404  ac6sfi  6421  enq0tr  6675  distrlem4prl  6825  distrlem4pru  6826  ltaprg  6860  lelttr  7255  ltletr  7256  readdcan  7304  addcan  7344  addcan2  7345  ltadd2  7579  divmulassap  7839  xrlelttr  8941  xrltletr  8942  icoshftf1o  9078  difelfzle  9211  fzo1fzo0n0  9258  modqmuladdim  9438  modqmuladdnn0  9439  modqm1p1mod0  9446  q2submod  9456  modifeq2int  9457  modqaddmulmod  9462  ltexp2a  9614  exple1  9618  expnlbnd2  9684  expcan  9730  maxleastb  10227  maxltsup  10231  addcn2  10276  mulcn2  10278  modmulconst  10361  dvdsmod  10396  divalglemex  10455  divalg  10457  gcdass  10537  rplpwr  10549  rppwr  10550  rpmulgcd2  10610  rpdvds  10614  rpexp  10665  znege1  10689