Theorem simpl3 1004

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

Assertion

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

Proof of Theorem simpl3

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpll3  1040  simprl3  1046  simp1l3  1094  simp2l3  1100  simp3l3  1106  3anandirs  1359  frirrg  4365  fcofo  5801  acexmid  5890  rdgon  6405  oawordi  6488  nnmord  6536  nnmword  6537  fidifsnen  6888  dif1en  6897  ac6sfi  6916  difinfsn  7117  2omotaplemap  7274  enq0tr  7451  distrlem4prl  7601  distrlem4pru  7602  ltaprg  7636  lelttr  8064  ltletr  8065  readdcan  8115  addcan  8155  addcan2  8156  ltadd2  8394  divmulassap  8670  xrlelttr  9824  xrltletr  9825  xaddass  9887  xleadd1a  9891  xlesubadd  9901  icoshftf1o  10009  difelfzle  10152  fzo1fzo0n0  10201  modqmuladdim  10385  modqmuladdnn0  10386  modqm1p1mod0  10393  q2submod  10403  modifeq2int  10404  modqaddmulmod  10409  ltexp2a  10590  exple1  10594  expnlbnd2  10664  nn0ltexp2  10707  nn0leexp2  10708  mulsubdivbinom2ap  10709  expcan  10714  fiprsshashgt1  10815  maxleastb  11241  maxltsup  11245  xrltmaxsup  11283  xrmaxltsup  11284  xrmaxaddlem  11286  xrmaxadd  11287  addcn2  11336  mulcn2  11338  isumz  11415  dvdsmodexp  11820  modmulconst  11848  dvdsmod  11886  divalglemex  11945  divalg  11947  gcdass  12034  rplpwr  12046  rppwr  12047  nnwodc  12055  uzwodc  12056  rpmulgcd2  12113  rpdvds  12117  rpexp  12171  znege1  12196  prmdiveq  12254  hashgcdlem  12256  coprimeprodsq  12275  coprimeprodsq2  12276  pythagtriplem3  12285  pcdvdsb  12337  pcgcd1  12345  dvdsprmpweq  12352  pcbc  12367  ctinf  12449  nninfdc  12472  isnsgrp  12835  issubmnd  12869  mulgnn0p1  13039  mulgnnsubcl  13040  mulgneg  13046  mulgdirlem  13059  nmzsubg  13115  ghmmulg  13156  ring1eq0  13361  rmodislmod  13628  lspss  13676  2idlcpblrng  13799  neiint  14042  topssnei  14059  cnptopco  14119  cnrest2  14133  cnptoprest  14136  upxp  14169  bldisj  14298  blgt0  14299  bl2in  14300  blss2ps  14303  blss2  14304  xblm  14314  blssps  14324  blss  14325  bdmopn  14401  metcnp2  14410  txmetcnp  14415  cncfmptc  14479  dvcnp2cntop  14560  dvcn  14561  logdivlti  14699  ltexp2  14757  lgsfvalg  14803  lgsneg  14822  lgsmod  14824  lgsdilem  14825  lgsdirprm  14832  lgsdir  14833  lgsdi  14835  lgsne0  14836  1dom1el  15140