Theorem simpl3 992

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

Assertion

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

Proof of Theorem simpl3

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

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

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 970

This theorem is referenced by:  simpll3  1028  simprl3  1034  simp1l3  1082  simp2l3  1088  simp3l3  1094  3anandirs  1338  frirrg  4327  fcofo  5751  acexmid  5840  rdgon  6350  oawordi  6433  nnmord  6481  nnmword  6482  fidifsnen  6832  dif1en  6841  ac6sfi  6860  difinfsn  7061  enq0tr  7371  distrlem4prl  7521  distrlem4pru  7522  ltaprg  7556  lelttr  7983  ltletr  7984  readdcan  8034  addcan  8074  addcan2  8075  ltadd2  8313  divmulassap  8587  xrlelttr  9738  xrltletr  9739  xaddass  9801  xleadd1a  9805  xlesubadd  9815  icoshftf1o  9923  difelfzle  10065  fzo1fzo0n0  10114  modqmuladdim  10298  modqmuladdnn0  10299  modqm1p1mod0  10306  q2submod  10316  modifeq2int  10317  modqaddmulmod  10322  ltexp2a  10503  exple1  10507  expnlbnd2  10576  nn0ltexp2  10619  nn0leexp2  10620  expcan  10625  fiprsshashgt1  10726  maxleastb  11152  maxltsup  11156  xrltmaxsup  11194  xrmaxltsup  11195  xrmaxaddlem  11197  xrmaxadd  11198  addcn2  11247  mulcn2  11249  isumz  11326  dvdsmodexp  11731  modmulconst  11759  dvdsmod  11796  divalglemex  11855  divalg  11857  gcdass  11944  rplpwr  11956  rppwr  11957  nnwodc  11965  uzwodc  11966  rpmulgcd2  12023  rpdvds  12027  rpexp  12081  znege1  12106  prmdiveq  12164  hashgcdlem  12166  coprimeprodsq  12185  coprimeprodsq2  12186  pythagtriplem3  12195  pcdvdsb  12247  pcgcd1  12255  dvdsprmpweq  12262  pcbc  12277  ctinf  12359  nninfdc  12382  neiint  12745  topssnei  12762  cnptopco  12822  cnrest2  12836  cnptoprest  12839  upxp  12872  bldisj  13001  blgt0  13002  bl2in  13003  blss2ps  13006  blss2  13007  xblm  13017  blssps  13027  blss  13028  bdmopn  13104  metcnp2  13113  txmetcnp  13118  cncfmptc  13182  dvcnp2cntop  13263  dvcn  13264  logdivlti  13402  ltexp2  13460  lgsfvalg  13506  lgsneg  13525  lgsmod  13527  lgsdilem  13528  lgsdirprm  13535  lgsdir  13536  lgsdi  13538  lgsne0  13539