Theorem mp3an 1464

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 1451	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 693	1 ⊢ 𝜃

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  el3v  3447  raltp  4661  rextp  4662  opthhausdorff  5464  funopg  6525  feq12i  6654  ftp  7102  caovass  7558  caovdi  7577  ordom  7818  mptexw  7897  ofmres  7928  sbcoteq1a  7995  mpoexw  8022  xpord3lem  8091  omopthlem1  8587  omopthlem2  8588  omopthi  8589  on2recsfn  8595  xpcomen  8998  snnen2o  9147  unfilem3  9209  hartogs  9451  card2on  9461  unwf  9724  inlresf1  9829  inrresf1  9831  tskwe  9864  alephsmo  10014  dfac4  10034  dfac2a  10042  ackbij1lem13  10143  axdc2lem  10360  axcclem  10369  ondomon  10475  cfpwsdom  10497  pwfseqlem2  10572  pwfseqlem3  10573  1lt2pi  10818  addassi  11144  mulassi  11145  adddii  11146  adddiri  11147  lttri  11261  lelttri  11262  ltletri  11263  letri  11264  ltadd2i  11266  mul02lem2  11312  addrid  11315  addcani  11328  addcan2i  11329  mul12i  11330  mul32i  11331  add12i  11358  add32i  11359  subaddi  11470  subadd2i  11471  subsub23i  11473  addsubassi  11474  addsubi  11475  subcani  11476  subcan2i  11477  pnncani  11478  subdii  11588  subdiri  11589  ltadd1i  11693  leadd1i  11694  leadd2i  11695  ltsubaddi  11696  lesubaddi  11697  ltsubadd2i  11698  lesubadd2i  11699  ltaddsubi  11700  mulcani  11778  div23i  11901  div11i  11902  3halfnz  12573  mpoaddex  12903  addex  12904  mpomulex  12905  mulex  12906  unirnioo  13367  ioorebas  13369  xnn0xrge0  13424  fldiv4lem1div2  13759  uzenom  13889  nnenom  13905  seqexw  13942  m1expcl2  14010  i4  14129  expnass  14133  faclbnd4lem1  14218  bcn1  14238  hashfxnn0  14262  ccat2s1p1  14555  ccat2s1p2  14556  cats1fvn  14783  cats1fv  14784  cats1cat  14786  cats2cat  14787  wrdlen3s3  14874  abs3difi  15335  0.999...  15806  bpoly3  15983  ef01bndlem  16111  cos1bnd  16114  cos2bnd  16115  sin4lt0  16122  rpnnen2lem3  16143  rpnnen2lem11  16151  rpnnen  16154  rexpen  16155  aleph1irr  16173  3dvdsdec  16261  3dvds2dec  16262  divalglem2  16324  ndvdsi  16341  flodddiv4  16344  gcdaddmlem  16453  bezout  16472  3lcm2e6woprm  16544  6lcm4e12  16545  lcmf0  16563  lcmf2a3a4e12  16576  dec2dvds  16993  modxai  16998  modsubi  17002  gcdi  17003  numexp2x  17008  2exp5  17015  2exp11  17019  ex-chn2  18563  0symgefmndeq  19325  pmtrprfval  19418  m1expaddsub  19429  0frgp  19710  staffval  20776  cnfldcj  21320  cnfldds  21323  cnfldfunALT  21326  cnfldcjOLD  21333  cnflddsOLD  21336  cnfldfunALTOLD  21339  xrsadd  21342  xrsmul  21343  xrsds  21366  cnmgpid  21386  nn0srg  21394  rge0srg  21395  zring0  21415  pzriprnglem13  21450  pzriprng1ALT  21453  fermltlchr  21486  cnmsgnsubg  21534  psgninv  21539  re0g  21569  ocvfval  21623  frlmbas  21712  mdetrlin  22548  mdetunilem9  22566  leordtval2  23158  iscnp2  23185  utop3cls  24197  nmfval  24534  nmoffn  24657  nmofval  24660  icccld  24712  addcnlem  24811  iimulcn  24892  iimulcnOLD  24893  icopnfhmeo  24899  iccpnfcnv  24900  iccpnfhmeo  24901  xrhmeo  24902  xrhmph  24903  oprpiece1res1  24907  oprpiece1res2  24908  ishtpy  24929  pcoass  24982  cnstrcvs  25099  cncvs  25103  recvs  25104  qcvs  25105  zclmncvs  25106  tcphex  25175  cnfldcusp  25315  resscdrg  25316  reust  25339  recusp  25340  vitalilem4  25570  vitalilem5  25571  mbfdm  25585  dveflem  25941  dvlipcn  25957  c1lip2  25961  dgrid  26228  iaa  26291  abelthlem3  26401  abelthlem5  26403  abelth  26409  efcn  26411  sinhalfpilem  26430  sincosq1lem  26464  sincosq4sgn  26468  tangtx  26472  sincos4thpi  26480  sincos6thpi  26483  pigt3  26485  pige3ALT  26487  cos0pilt1  26499  logi  26554  relogcn  26605  dvlog2lem  26619  dvlog2  26620  logtayl  26627  logtayl2  26629  cxpsqrtlem  26669  cxpsqrt  26670  2irrexpq  26698  cxpcn2  26714  cxpcn3  26716  logblog  26760  2logb9irr  26763  2logb3irr  26765  2logb9irrALT  26766  sqrt2cxp2logb9e3  26767  2irrexpqALT  26768  ang180lem1  26777  ang180lem2  26778  1cubrlem  26809  mcubic  26815  quart1lem  26823  quart1  26824  reasinsin  26864  atancj  26878  efiatan  26880  atantan  26891  atanbndlem  26893  atan1  26896  atancn  26904  atantayl2  26906  log2cnv  26912  log2tlbnd  26913  log2ublem1  26914  log2ublem2  26915  log2ub  26917  efrlim  26937  efrlimOLD  26938  scvxcvx  26954  1sgm2ppw  27169  ppiub  27173  bclbnd  27249  bposlem8  27260  lgsdir2lem1  27294  lgsdir2lem5  27298  lgseisenlem1  27344  lgseisenlem2  27345  lgsquadlem1  27349  chebbnd1  27441  dchrvmasumlem2  27467  norecfn  27926  norec2fn  27936  addsproplem2  27950  addsproplem6  27954  addsbdaylem  27997  negs1s  28007  negsproplem2  28009  mulsproplem2  28097  mulsproplem3  28098  mulsproplem5  28100  mulsproplem6  28101  mulsproplem7  28102  mulsproplem8  28103  mulsproplem13  28108  mulsproplem14  28109  0zs  28365  zseo  28399  twocut  28400  bdaypw2n0sbndlem  28440  bdaypw2bnd  28442  bdayfinbndlem1  28444  zs12bdaylem2  28448  istrkg3ld  28514  trgcgrg  28568  ax5seglem7  28989  axlowdimlem6  29001  axlowdimlem8  29003  axlowdimlem11  29006  elntg2  29039  cusgrsizeindb1  29505  vtxdginducedm1  29598  0grrusgr  29634  erclwwlktr  30078  erclwwlkntr  30127  wlk2v2e  30213  upgr3v3e3cycl  30236  konigsberglem1  30308  konigsberglem2  30309  konigsberglem3  30310  konigsberglem5  30312  ex-fl  30503  ex-mod  30505  ex-hash  30509  ex-lcm  30514  0vfval  30662  smcnlem  30753  lnocoi  30813  nmlno0lem  30849  nmblolbii  30855  blocnilem  30860  blocni  30861  cncph  30875  isph  30878  ip0i  30881  ip1ilem  30882  ip2i  30884  ipdirilem  30885  ipasslem7  30892  ipasslem8  30893  ipasslem9  30894  ipasslem10  30895  ipasslem11  30896  ip2dii  30900  pythi  30906  siilem1  30907  siilem2  30908  siii  30909  hvmulassi  31102  hvmulcomi  31103  hvdistr1i  31107  hvsubdistr1i  31108  hvassi  31109  hvadd32i  31110  hvsubassi  31111  hvsub32i  31112  normlem0  31165  normlem8  31173  normlem9  31174  bcseqi  31176  polid2i  31213  hhph  31234  hlim0  31291  shscli  31373  shlessi  31433  shlej1i  31434  omlsilem  31458  shlubi  31471  h1de2i  31609  pjadjii  31730  pjaddii  31731  pjmulii  31733  pjdifnormii  31739  pjcji  31740  hoaddsubassi  31876  eigrei  31890  eigposi  31892  eigorthi  31893  adj0  32050  lnopeq0lem1  32061  lnopunilem1  32066  lnophmlem2  32073  nmcexi  32082  nmcopexi  32083  lnfn0i  32098  nmcfnexi  32107  mdexchi  32391  xppreima2  32709  sgnclre  32892  dp2clq  32941  dp2lt  32945  dp2ltc  32947  dpexpp1  32968  dpmul  32973  dpmul4  32974  elxrge02  32992  xrge0adddir  33079  psgnid  33158  cnmsgn0g  33207  altgnsg  33210  xrnarchi  33245  xrge0slmod  33408  znfermltl  33426  ccfldextdgrr  33808  cos9thpiminplylem4  33921  cos9thpiminplylem5  33922  raddcn  34065  xrge0iifcnv  34069  xrge0iifiso  34071  xrge0iifhmeo  34072  xrge0iifhom  34073  xrge0iifmhm  34075  xrge0mulc1cn  34077  lmlimxrge0  34084  pnfneige0  34087  lmxrge0  34088  zringnm  34094  rezh  34105  qqh0  34120  qqh1  34121  qqhucn  34128  esumpinfval  34209  hashf2  34220  esumcvg  34222  br2base  34405  sxbrsigalem3  34408  dya2iocbrsiga  34411  dya2icobrsiga  34412  sxbrsigalem1  34421  sxbrsigalem2  34422  sxbrsigalem4  34423  sxbrsigalem5  34424  sxbrsiga  34426  ballotlem2  34625  ballotlem4  34635  ballotlemi1  34639  ballotth  34674  signstf  34702  itgexpif  34742  chtvalz  34765  hgt750lemd  34784  hgt750lem  34787  tgoldbachgnn  34795  lfuhgr2  35292  subfacp1lem1  35352  subfacp1lem6  35358  kur14lem6  35384  cvmliftlem4  35461  satf0suc  35549  problem4  35841  quad3  35843  iexpire  35908  fununiq  35942  fvtransport  36205  bj-minftyccb  37399  taupilem2  37496  iccioo01  37501  1oequni2o  37542  finxp1o  37566  finxpreclem4  37568  cos2h  37781  tan2h  37782  poimirlem9  37799  poimirlem27  37817  poimirlem28  37818  ismblfin  37831  mbfposadd  37837  ftc1anclem5  37867  asindmre  37873  dvasin  37874  dvacos  37875  rrnval  37997  dihjatcclem4  41716  lcmineqlem12  42329  fisdomnn  42536  subex  42539  absex  42540  cjex  42541  cxpi11d  42635  redvmptabs  42652  readvrec  42654  sn-00idlem2  42691  sn-00id  42693  remul02  42697  rabren3dioph  43094  jm2.27dlem2  43289  rmydioph  43293  rmxdioph  43295  expdiophlem2  43301  expdioph  43302  arearect  43494  areaquad  43495  2omomeqom  43582  omnord1ex  43583  corclrcl  43985  iunrelexpuztr  43997  corcltrcl  44017  dffrege76  44217  k0004val0  44432  lhe4.4ex1a  44607  binomcxplemdvbinom  44631  binomcxplemnotnn0  44634  ax6e2ndeqALT  45208  sineq0ALT  45214  nregmodelf1o  45293  pnfel0pnf  45811  lptioo2cn  45926  limsup10ex  46054  liminf10ex  46055  icccncfext  46168  itgsin0pilem1  46231  itgsbtaddcnst  46263  stoweidlem13  46294  wallispilem2  46347  wallispilem4  46349  wallispi2lem1  46352  stirlinglem13  46367  dirkerper  46377  dirkertrigeqlem3  46381  dirkeritg  46383  dirkercncflem1  46384  dirkercncflem4  46387  fourierdlem42  46430  fourierdlem62  46449  fourierdlem102  46489  fourierdlem103  46490  fourierdlem104  46491  fourierdlem114  46501  sqwvfoura  46509  fourierswlem  46511  fouriersw  46512  smfmullem4  47075  nthrucw  47167  ceil5half3  47623  8mod5e3  47643  fmtnoprmfac2lem1  47849  fmtno4prm  47858  3exp4mod41  47899  41prothprmlem2  47901  6gbe  48054  7gbow  48055  8gbe  48056  9gbo  48057  11gbo  48058  sbgoldbalt  48064  nnsum4primesevenALTV  48084  usgrexmpl2nb0  48314  usgrexmpl2nb3  48317  gpg3nbgrvtx0  48359  gpg3nbgrvtx0ALT  48360  gpg3nbgrvtx1  48361  gpg5grlim  48376  gpg5grlic  48377  0nodd  48453  oddinmgm  48458  2zrng0  48527  zlmodzxz0  48639  zlmodzxzequa  48779  zlmodzxzequap  48782  zlmodzxzldeplem3  48785  nnlog2ge0lt1  48849  blen1  48867  blen2  48868  nnolog2flm1  48873  ackval42  48979  ehl2eudisval0  49008  line2ylem  49034  i0oii  49202  io1ii  49203  sepfsepc  49210  rescofuf  49375  setc1ohomfval  49775  setc1ocofval  49776