Theorem simpl3 986

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

Assertion

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

Proof of Theorem simpl3

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simpll3  1022  simprl3  1028  simp1l3  1076  simp2l3  1082  simp3l3  1088  3anandirs  1326  frirrg  4267  fcofo  5678  acexmid  5766  rdgon  6276  oawordi  6358  nnmord  6406  nnmword  6407  fidifsnen  6757  dif1en  6766  ac6sfi  6785  difinfsn  6978  enq0tr  7235  distrlem4prl  7385  distrlem4pru  7386  ltaprg  7420  lelttr  7845  ltletr  7846  readdcan  7895  addcan  7935  addcan2  7936  ltadd2  8174  divmulassap  8448  xrlelttr  9582  xrltletr  9583  xaddass  9645  xleadd1a  9649  xlesubadd  9659  icoshftf1o  9767  difelfzle  9904  fzo1fzo0n0  9953  modqmuladdim  10133  modqmuladdnn0  10134  modqm1p1mod0  10141  q2submod  10151  modifeq2int  10152  modqaddmulmod  10157  ltexp2a  10338  exple1  10342  expnlbnd2  10410  expcan  10456  fiprsshashgt1  10556  maxleastb  10979  maxltsup  10983  xrltmaxsup  11019  xrmaxltsup  11020  xrmaxaddlem  11022  xrmaxadd  11023  addcn2  11072  mulcn2  11074  isumz  11151  modmulconst  11514  dvdsmod  11549  divalglemex  11608  divalg  11610  gcdass  11692  rplpwr  11704  rppwr  11705  rpmulgcd2  11765  rpdvds  11769  rpexp  11820  znege1  11845  hashgcdlem  11892  ctinf  11932  neiint  12303  topssnei  12320  cnptopco  12380  cnrest2  12394  cnptoprest  12397  upxp  12430  bldisj  12559  blgt0  12560  bl2in  12561  blss2ps  12564  blss2  12565  xblm  12575  blssps  12585  blss  12586  bdmopn  12662  metcnp2  12671  txmetcnp  12676  cncfmptc  12740  dvcnp2cntop  12821  dvcn  12822