Theorem simpl3 987

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

Assertion

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

Proof of Theorem simpl3

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

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

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 965

This theorem is referenced by:  simpll3  1023  simprl3  1029  simp1l3  1077  simp2l3  1083  simp3l3  1089  3anandirs  1327  frirrg  4280  fcofo  5693  acexmid  5781  rdgon  6291  oawordi  6373  nnmord  6421  nnmword  6422  fidifsnen  6772  dif1en  6781  ac6sfi  6800  difinfsn  6993  enq0tr  7266  distrlem4prl  7416  distrlem4pru  7417  ltaprg  7451  lelttr  7876  ltletr  7877  readdcan  7926  addcan  7966  addcan2  7967  ltadd2  8205  divmulassap  8479  xrlelttr  9619  xrltletr  9620  xaddass  9682  xleadd1a  9686  xlesubadd  9696  icoshftf1o  9804  difelfzle  9942  fzo1fzo0n0  9991  modqmuladdim  10171  modqmuladdnn0  10172  modqm1p1mod0  10179  q2submod  10189  modifeq2int  10190  modqaddmulmod  10195  ltexp2a  10376  exple1  10380  expnlbnd2  10448  expcan  10494  fiprsshashgt1  10595  maxleastb  11018  maxltsup  11022  xrltmaxsup  11058  xrmaxltsup  11059  xrmaxaddlem  11061  xrmaxadd  11062  addcn2  11111  mulcn2  11113  isumz  11190  modmulconst  11561  dvdsmod  11596  divalglemex  11655  divalg  11657  gcdass  11739  rplpwr  11751  rppwr  11752  rpmulgcd2  11812  rpdvds  11816  rpexp  11867  znege1  11892  hashgcdlem  11939  ctinf  11979  neiint  12353  topssnei  12370  cnptopco  12430  cnrest2  12444  cnptoprest  12447  upxp  12480  bldisj  12609  blgt0  12610  bl2in  12611  blss2ps  12614  blss2  12615  xblm  12625  blssps  12635  blss  12636  bdmopn  12712  metcnp2  12721  txmetcnp  12726  cncfmptc  12790  dvcnp2cntop  12871  dvcn  12872  logdivlti  13010