Theorem mp3an 1470

Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
mp3an.1	⊢ 𝜑
mp3an.2	⊢ 𝜓
mp3an.3	⊢ 𝜒
mp3an.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an	⊢ 𝜃

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 ⊢ 𝜓
2		mp3an.3	. 2 ⊢ 𝜒
3		mp3an.1	. . 3 ⊢ 𝜑
4		mp3an.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
5	3, 4	mp3an1 1457	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 699	1 ⊢ 𝜃

Syntax hints:   → wi 4   ∧ w3a 1093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095

This theorem is referenced by:  el3v  3441  raltp  4639  rextp  4640  opthhausdorff  5460  funopg  6522  feq12i  6651  ftp  7103  caovass  7559  caovdi  7578  ordom  7819  mptexw  7897  ofmres  7928  sbcoteq1a  7995  mpoexw  8022  xpord3lem  8091  omopthlem1  8589  omopthlem2  8590  omopthi  8591  on2recsfn  8597  xpcomen  9000  snnen2o  9149  unfilem3  9211  hartogs  9453  card2on  9463  unwf  9729  inlresf1  9834  inrresf1  9836  tskwe  9869  alephsmo  10019  dfac4  10039  dfac2a  10047  ackbij1lem13  10148  axdc2lem  10366  axcclem  10375  ondomon  10481  cfpwsdom  10503  pwfseqlem2  10578  pwfseqlem3  10579  1lt2pi  10824  addassi  11151  mulassi  11152  adddii  11153  adddiri  11154  lttri  11268  lelttri  11269  ltletri  11270  letri  11271  ltadd2i  11273  mul02lem2  11319  addrid  11322  addcani  11335  addcan2i  11336  mul12i  11337  mul32i  11338  add12i  11365  add32i  11366  subaddi  11477  subadd2i  11478  subsub23i  11480  addsubassi  11481  addsubi  11482  subcani  11483  subcan2i  11484  pnncani  11485  subdii  11595  subdiri  11596  ltadd1i  11700  leadd1i  11701  leadd2i  11702  ltsubaddi  11703  lesubaddi  11704  ltsubadd2i  11705  lesubadd2i  11706  ltaddsubi  11707  mulcani  11785  div23i  11908  div11i  11909  3halfnz  12603  mpoaddex  12933  addex  12934  mpomulex  12935  mulex  12936  unirnioo  13397  ioorebas  13399  xnn0xrge0  13454  fldiv4lem1div2  13791  uzenom  13921  nnenom  13937  seqexw  13974  m1expcl2  14042  i4  14161  expnass  14165  faclbnd4lem1  14250  bcn1  14270  hashfxnn0  14294  ccat2s1p1  14587  ccat2s1p2  14588  cats1fvn  14815  cats1fv  14816  cats1cat  14818  cats2cat  14819  wrdlen3s3  14906  abs3difi  15367  0.999...  15841  bpoly3  16018  ef01bndlem  16146  cos1bnd  16149  cos2bnd  16150  sin4lt0  16157  rpnnen2lem3  16178  rpnnen2lem11  16186  rpnnen  16189  rexpen  16190  aleph1irr  16208  3dvdsdec  16296  3dvds2dec  16297  divalglem2  16359  ndvdsi  16376  flodddiv4  16379  gcdaddmlem  16488  bezout  16507  3lcm2e6woprm  16579  6lcm4e12  16580  lcmf0  16598  lcmf2a3a4e12  16611  dec2dvds  17029  modxai  17034  modsubi  17038  gcdi  17039  numexp2x  17044  2exp5  17051  2exp11  17055  ex-chn2  18599  0symgefmndeq  19363  pmtrprfval  19456  m1expaddsub  19467  0frgp  19748  staffval  20816  cnfldcj  21359  cnfldds  21362  cnfldfunALT  21365  xrsadd  21368  xrsmul  21369  xrsds  21388  cnmgpid  21407  nn0srg  21415  rge0srg  21416  zring0  21436  pzriprnglem13  21471  pzriprng1ALT  21474  fermltlchr  21507  cnmsgnsubg  21555  psgninv  21560  re0g  21590  ocvfval  21644  frlmbas  21733  mdetrlin  22588  mdetunilem9  22606  leordtval2  23198  iscnp2  23225  utop3cls  24237  nmfval  24574  nmoffn  24697  nmofval  24700  icccld  24752  addcnlem  24851  iimulcn  24926  icopnfhmeo  24931  iccpnfcnv  24932  iccpnfhmeo  24933  xrhmeo  24934  xrhmph  24935  oprpiece1res1  24939  oprpiece1res2  24940  ishtpy  24960  pcoass  25012  cnstrcvs  25129  cncvs  25133  recvs  25134  qcvs  25135  zclmncvs  25136  tcphex  25205  cnfldcusp  25345  resscdrg  25346  reust  25369  recusp  25370  vitalilem4  25599  vitalilem5  25600  mbfdm  25614  dveflem  25967  dvlipcn  25982  c1lip2  25986  dgrid  26250  iaa  26312  abelthlem3  26419  abelthlem5  26421  abelth  26427  efcn  26429  sinhalfpilem  26448  sincosq1lem  26482  sincosq4sgn  26486  tangtx  26490  sincos4thpi  26498  sincos6thpi  26501  pigt3  26503  pige3ALT  26505  cos0pilt1  26517  logi  26572  relogcn  26623  dvlog2lem  26637  dvlog2  26638  logtayl  26645  logtayl2  26647  cxpsqrtlem  26687  cxpsqrt  26688  2irrexpq  26716  cxpcn2  26731  cxpcn3  26733  logblog  26777  2logb9irr  26780  2logb3irr  26782  2logb9irrALT  26783  sqrt2cxp2logb9e3  26784  2irrexpqALT  26785  ang180lem1  26794  ang180lem2  26795  1cubrlem  26826  mcubic  26832  quart1lem  26840  quart1  26841  reasinsin  26881  atancj  26895  efiatan  26897  atantan  26908  atanbndlem  26910  atan1  26913  atancn  26921  atantayl2  26923  log2cnv  26929  log2tlbnd  26930  log2ublem1  26931  log2ublem2  26932  log2ub  26934  efrlim  26954  scvxcvx  26970  1sgm2ppw  27184  ppiub  27188  bclbnd  27264  bposlem8  27275  lgsdir2lem1  27309  lgsdir2lem5  27313  lgseisenlem1  27359  lgseisenlem2  27360  lgsquadlem1  27364  chebbnd1  27456  dchrvmasumlem2  27482  norecfn  27958  norec2fn  27968  addsproplem2  27982  addsproplem6  27986  addbdaylem  28029  neg1s  28039  negsproplem2  28041  mulsproplem2  28129  mulsproplem3  28130  mulsproplem5  28132  mulsproplem6  28133  mulsproplem7  28134  mulsproplem8  28135  mulsproplem13  28140  mulsproplem14  28141  0zs  28400  zseo  28434  twocut  28435  bdaypw2n0bndlem  28475  bdaypw2bnd  28477  bdayfinbndlem1  28479  z12bdaylem2  28483  istrkg3ld  28549  trgcgrg  28603  ax5seglem7  29024  axlowdimlem6  29036  axlowdimlem8  29038  axlowdimlem11  29041  elntg2  29074  cusgrsizeindb1  29539  vtxdginducedm1  29632  0grrusgr  29668  erclwwlktr  30112  erclwwlkntr  30161  wlk2v2e  30247  upgr3v3e3cycl  30270  konigsberglem1  30342  konigsberglem2  30343  konigsberglem3  30344  konigsberglem5  30346  ex-fl  30537  ex-mod  30539  ex-hash  30543  ex-lcm  30548  0vfval  30697  smcnlem  30788  lnocoi  30848  nmlno0lem  30884  nmblolbii  30890  blocnilem  30895  blocni  30896  cncph  30910  isph  30913  ip0i  30916  ip1ilem  30917  ip2i  30919  ipdirilem  30920  ipasslem7  30927  ipasslem8  30928  ipasslem9  30929  ipasslem10  30930  ipasslem11  30931  ip2dii  30935  pythi  30941  siilem1  30942  siilem2  30943  siii  30944  hvmulassi  31137  hvmulcomi  31138  hvdistr1i  31142  hvsubdistr1i  31143  hvassi  31144  hvadd32i  31145  hvsubassi  31146  hvsub32i  31147  normlem0  31200  normlem8  31208  normlem9  31209  bcseqi  31211  polid2i  31248  hhph  31269  hlim0  31326  shscli  31408  shlessi  31468  shlej1i  31469  omlsilem  31493  shlubi  31506  h1de2i  31644  pjadjii  31765  pjaddii  31766  pjmulii  31768  pjdifnormii  31774  pjcji  31775  hoaddsubassi  31911  eigrei  31925  eigposi  31927  eigorthi  31928  adj0  32085  lnopeq0lem1  32096  lnopunilem1  32101  lnophmlem2  32108  nmcexi  32117  nmcopexi  32118  lnfn0i  32133  nmcfnexi  32142  mdexchi  32426  xppreima2  32745  sgnclre  32926  dp2clq  32961  dp2lt  32965  dp2ltc  32967  dpexpp1  32988  dpmul  32993  dpmul4  32994  elxrge02  33012  xrge0adddir  33099  psgnid  33180  cnmsgn0g  33229  altgnsg  33232  xrnarchi  33267  xrge0slmod  33433  znfermltl  33451  ccfldextdgrr  33866  cos9thpiminplylem4  33979  cos9thpiminplylem5  33980  raddcn  34123  xrge0iifcnv  34127  xrge0iifiso  34129  xrge0iifhmeo  34130  xrge0iifhom  34131  xrge0iifmhm  34133  xrge0mulc1cn  34135  lmlimxrge0  34142  pnfneige0  34145  lmxrge0  34146  zringnm  34152  rezh  34163  qqh0  34178  qqh1  34179  qqhucn  34186  esumpinfval  34267  hashf2  34278  esumcvg  34280  br2base  34463  sxbrsigalem3  34466  dya2iocbrsiga  34469  dya2icobrsiga  34470  sxbrsigalem1  34479  sxbrsigalem2  34480  sxbrsigalem4  34481  sxbrsigalem5  34482  sxbrsiga  34484  ballotlem2  34683  ballotlem4  34693  ballotlemi1  34697  ballotth  34732  signstf  34760  itgexpif  34800  chtvalz  34823  hgt750lemd  34842  hgt750lem  34845  tgoldbachgnn  34853  lfuhgr2  35360  subfacp1lem1  35420  subfacp1lem6  35426  kur14lem6  35452  cvmliftlem4  35529  satf0suc  35617  problem4  35909  quad3  35911  iexpire  35976  fununiq  36010  fvtransport  36273  ttcid  36733  dfttc2g  36747  bj-minftyccb  37598  taupilem2  37695  iccioo01  37702  1oequni2o  37743  finxp1o  37767  finxpreclem4  37769  cos2h  37991  tan2h  37992  poimirlem9  38009  poimirlem27  38027  poimirlem28  38028  ismblfin  38041  mbfposadd  38047  ftc1anclem5  38077  asindmre  38083  dvasin  38084  dvacos  38085  rrnval  38207  dihjatcclem4  41926  lcmineqlem12  42538  fisdomnn  42741  subex  42744  absex  42745  cjex  42746  cxpi11d  42833  redvmptabs  42850  readvrec  42852  sn-00idlem2  42889  sn-00id  42891  remul02  42895  rabren3dioph  43273  jm2.27dlem2  43468  rmydioph  43472  rmxdioph  43474  expdiophlem2  43480  expdioph  43481  arearect  43673  areaquad  43674  2omomeqom  43761  omnord1ex  43762  corclrcl  44164  iunrelexpuztr  44176  corcltrcl  44196  dffrege76  44396  k0004val0  44611  lhe4.4ex1a  44786  binomcxplemdvbinom  44810  binomcxplemnotnn0  44813  ax6e2ndeqALT  45387  sineq0ALT  45393  nregmodelf1o  45472  pnfel0pnf  45985  lptioo2cn  46100  limsup10ex  46228  liminf10ex  46229  icccncfext  46342  itgsin0pilem1  46405  itgsbtaddcnst  46437  stoweidlem13  46468  wallispilem2  46521  wallispilem4  46523  wallispi2lem1  46526  stirlinglem13  46541  dirkerper  46551  dirkertrigeqlem3  46555  dirkeritg  46557  dirkercncflem1  46558  dirkercncflem4  46561  fourierdlem42  46604  fourierdlem62  46623  fourierdlem102  46663  fourierdlem103  46664  fourierdlem104  46665  fourierdlem114  46675  sqwvfoura  46683  fourierswlem  46685  fouriersw  46686  smfmullem4  47249  nthrucw  47343  goldracos5teq  47360  goldratmolem2  47361  ceil5half3  47821  8mod5e3  47841  fmtnoprmfac2lem1  48056  fmtno4prm  48065  3exp4mod41  48106  41prothprmlem2  48108  ppivalnn4  48117  6gbe  48274  7gbow  48275  8gbe  48276  9gbo  48277  11gbo  48278  sbgoldbalt  48284  nnsum4primesevenALTV  48304  usgrexmpl2nb0  48534  usgrexmpl2nb3  48537  gpg3nbgrvtx0  48579  gpg3nbgrvtx0ALT  48580  gpg3nbgrvtx1  48581  gpg5grlim  48596  gpg5grlic  48597  0nodd  48673  oddinmgm  48678  2zrng0  48747  zlmodzxz0  48859  zlmodzxzequa  48999  zlmodzxzequap  49002  zlmodzxzldeplem3  49005  nnlog2ge0lt1  49069  blen1  49087  blen2  49088  nnolog2flm1  49093  ackval42  49199  ehl2eudisval0  49228  line2ylem  49254  i0oii  49422  io1ii  49423  sepfsepc  49430  rescofuf  49595  setc1ohomfval  49995  setc1ocofval  49996