Theorem simpl3 943

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

Assertion

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

Proof of Theorem simpl3

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

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

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 921

This theorem is referenced by:  simpll3  979  simprl3  985  simp1l3  1033  simp2l3  1039  simp3l3  1045  3anandirs  1279  frirrg  4105  fcofo  5444  acexmid  5531  oawordi  6072  nnmord  6113  nnmword  6114  fidifsnen  6355  dif1en  6364  ac6sfi  6379  enq0tr  6624  distrlem4prl  6774  distrlem4pru  6775  ltaprg  6809  lelttr  7199  ltletr  7200  readdcan  7248  addcan  7288  addcan2  7289  ltadd2  7523  divmulassap  7783  xrlelttr  8876  xrltletr  8877  icoshftf1o  9013  difelfzle  9145  fzo1fzo0n0  9192  modqmuladdim  9369  modqmuladdnn0  9370  modqm1p1mod0  9377  q2submod  9387  modifeq2int  9388  modqaddmulmod  9393  ltexp2a  9528  exple1  9532  expnlbnd2  9598  expcan  9644  maxleastb  10100  maxltsup  10104  addcn2  10149  mulcn2  10151  modmulconst  10227  dvdsmod  10262  divalglemex  10322  divalg  10324  gcdass  10404  rplpwr  10416  rppwr  10417  rpmulgcd2  10477  rpdvds  10481  rpexp  10532  znege1  10556