Theorem mp3an 1463

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  el3v  3472  raltp  4686  rextp  4687  opthhausdorff  5497  funopg  6575  feq12i  6704  ftp  7152  caovass  7612  caovdi  7631  ordom  7876  mptexw  7956  ofmres  7988  sbcoteq1a  8055  mpoexw  8082  xpord3lem  8153  omopthlem1  8676  omopthlem2  8677  omopthi  8678  on2recsfn  8684  xpcomen  9082  snnen2o  9250  unfilem3  9322  hartogs  9563  card2on  9573  unwf  9829  inlresf1  9934  inrresf1  9936  tskwe  9969  alephsmo  10121  dfac4  10141  dfac2a  10149  ackbij1lem13  10250  axdc2lem  10467  axcclem  10476  ondomon  10582  cfpwsdom  10603  pwfseqlem2  10678  pwfseqlem3  10679  1lt2pi  10924  addassi  11250  mulassi  11251  adddii  11252  adddiri  11253  lttri  11366  lelttri  11367  ltletri  11368  letri  11369  ltadd2i  11371  mul02lem2  11417  addrid  11420  addcani  11433  addcan2i  11434  mul12i  11435  mul32i  11436  add12i  11463  add32i  11464  subaddi  11575  subadd2i  11576  subsub23i  11578  addsubassi  11579  addsubi  11580  subcani  11581  subcan2i  11582  pnncani  11583  subdii  11691  subdiri  11692  ltadd1i  11796  leadd1i  11797  leadd2i  11798  ltsubaddi  11799  lesubaddi  11800  ltsubadd2i  11801  lesubadd2i  11802  ltaddsubi  11803  mulcani  11881  div23i  12004  div11i  12005  3halfnz  12677  mpoaddex  13009  addex  13010  mpomulex  13011  mulex  13012  unirnioo  13471  ioorebas  13473  xnn0xrge0  13528  fldiv4lem1div2  13859  uzenom  13987  nnenom  14003  seqexw  14040  m1expcl2  14108  i4  14227  expnass  14231  faclbnd4lem1  14316  bcn1  14336  hashfxnn0  14360  ccat2s1p1  14652  ccat2s1p2  14653  cats1fvn  14882  cats1fv  14883  cats1cat  14885  cats2cat  14886  wrdlen3s3  14973  abs3difi  15433  0.999...  15902  bpoly3  16079  ef01bndlem  16207  cos1bnd  16210  cos2bnd  16211  sin4lt0  16218  rpnnen2lem3  16239  rpnnen2lem11  16247  rpnnen  16250  rexpen  16251  aleph1irr  16269  3dvdsdec  16356  3dvds2dec  16357  divalglem2  16419  ndvdsi  16436  flodddiv4  16439  gcdaddmlem  16548  bezout  16567  3lcm2e6woprm  16639  6lcm4e12  16640  lcmf0  16658  lcmf2a3a4e12  16671  dec2dvds  17088  modxai  17093  modsubi  17097  gcdi  17098  numexp2x  17103  2exp5  17110  2exp11  17114  0symgefmndeq  19380  pmtrprfval  19473  m1expaddsub  19484  0frgp  19765  staffval  20806  cnfldcj  21329  cnfldds  21332  cnfldfunALT  21335  cnfldcjOLD  21342  cnflddsOLD  21345  cnfldfunALTOLD  21348  xrsadd  21352  xrsmul  21353  xrsds  21382  cnmgpid  21402  nn0srg  21410  rge0srg  21411  zring0  21424  pzriprnglem13  21459  pzriprng1ALT  21462  fermltlchr  21495  cnmsgnsubg  21542  psgninv  21547  re0g  21577  ocvfval  21631  frlmbas  21720  mdetrlin  22545  mdetunilem9  22563  leordtval2  23155  iscnp2  23182  utop3cls  24195  nmfval  24532  nmoffn  24655  nmofval  24658  icccld  24710  addcnlem  24809  iimulcn  24890  iimulcnOLD  24891  icopnfhmeo  24897  iccpnfcnv  24898  iccpnfhmeo  24899  xrhmeo  24900  xrhmph  24901  oprpiece1res1  24905  oprpiece1res2  24906  ishtpy  24927  pcoass  24980  cnstrcvs  25097  cncvs  25101  recvs  25102  recvsOLD  25103  qcvs  25104  zclmncvs  25105  tcphex  25174  cnfldcusp  25314  resscdrg  25315  reust  25338  recusp  25339  vitalilem4  25569  vitalilem5  25570  mbfdm  25584  dveflem  25940  dvlipcn  25956  c1lip2  25960  dgrid  26227  iaa  26290  abelthlem3  26400  abelthlem5  26402  abelth  26408  efcn  26410  sinhalfpilem  26429  sincosq1lem  26463  sincosq4sgn  26467  tangtx  26471  sincos4thpi  26479  sincos6thpi  26482  pigt3  26484  pige3ALT  26486  cos0pilt1  26498  logi  26553  relogcn  26604  dvlog2lem  26618  dvlog2  26619  logtayl  26626  logtayl2  26628  cxpsqrtlem  26668  cxpsqrt  26669  2irrexpq  26697  cxpcn2  26713  cxpcn3  26715  logblog  26759  2logb9irr  26762  2logb3irr  26764  2logb9irrALT  26765  sqrt2cxp2logb9e3  26766  2irrexpqALT  26767  ang180lem1  26776  ang180lem2  26777  1cubrlem  26808  mcubic  26814  quart1lem  26822  quart1  26823  reasinsin  26863  atancj  26877  efiatan  26879  atantan  26890  atanbndlem  26892  atan1  26895  atancn  26903  atantayl2  26905  log2cnv  26911  log2tlbnd  26912  log2ublem1  26913  log2ublem2  26914  log2ub  26916  efrlim  26936  efrlimOLD  26937  scvxcvx  26953  1sgm2ppw  27168  ppiub  27172  bclbnd  27248  bposlem8  27259  lgsdir2lem1  27293  lgsdir2lem5  27297  lgseisenlem1  27343  lgseisenlem2  27344  lgsquadlem1  27348  chebbnd1  27440  dchrvmasumlem2  27466  norecfn  27910  norec2fn  27920  addsproplem2  27934  addsproplem6  27938  addsbdaylem  27980  negs1s  27990  negsproplem2  27992  mulsproplem2  28077  mulsproplem3  28078  mulsproplem5  28080  mulsproplem6  28081  mulsproplem7  28082  mulsproplem8  28083  mulsproplem13  28088  mulsproplem14  28089  0zs  28333  zseo  28365  twocut  28366  istrkg3ld  28445  trgcgrg  28499  ax5seglem7  28919  axlowdimlem6  28931  axlowdimlem8  28933  axlowdimlem11  28936  elntg2  28969  cusgrsizeindb1  29435  vtxdginducedm1  29528  0grrusgr  29564  erclwwlktr  30008  erclwwlkntr  30057  wlk2v2e  30143  upgr3v3e3cycl  30166  konigsberglem1  30238  konigsberglem2  30239  konigsberglem3  30240  konigsberglem5  30242  ex-fl  30433  ex-mod  30435  ex-hash  30439  ex-lcm  30444  0vfval  30592  smcnlem  30683  lnocoi  30743  nmlno0lem  30779  nmblolbii  30785  blocnilem  30790  blocni  30791  cncph  30805  isph  30808  ip0i  30811  ip1ilem  30812  ip2i  30814  ipdirilem  30815  ipasslem7  30822  ipasslem8  30823  ipasslem9  30824  ipasslem10  30825  ipasslem11  30826  ip2dii  30830  pythi  30836  siilem1  30837  siilem2  30838  siii  30839  hvmulassi  31032  hvmulcomi  31033  hvdistr1i  31037  hvsubdistr1i  31038  hvassi  31039  hvadd32i  31040  hvsubassi  31041  hvsub32i  31042  normlem0  31095  normlem8  31103  normlem9  31104  bcseqi  31106  polid2i  31143  hhph  31164  hlim0  31221  shscli  31303  shlessi  31363  shlej1i  31364  omlsilem  31388  shlubi  31401  h1de2i  31539  pjadjii  31660  pjaddii  31661  pjmulii  31663  pjdifnormii  31669  pjcji  31670  hoaddsubassi  31806  eigrei  31820  eigposi  31822  eigorthi  31823  adj0  31980  lnopeq0lem1  31991  lnopunilem1  31996  lnophmlem2  32003  nmcexi  32012  nmcopexi  32013  lnfn0i  32028  nmcfnexi  32037  mdexchi  32321  xppreima2  32634  sgnclre  32816  dp2clq  32860  dp2lt  32864  dp2ltc  32866  dpexpp1  32887  dpmul  32892  dpmul4  32893  elxrge02  32911  xrge0adddir  33018  psgnid  33113  cnmsgn0g  33162  altgnsg  33165  xrnarchi  33187  xrge0slmod  33368  znfermltl  33386  ccfldextdgrr  33718  cos9thpiminplylem4  33824  cos9thpiminplylem5  33825  raddcn  33965  xrge0iifcnv  33969  xrge0iifiso  33971  xrge0iifhmeo  33972  xrge0iifhom  33973  xrge0iifmhm  33975  xrge0mulc1cn  33977  lmlimxrge0  33984  pnfneige0  33987  lmxrge0  33988  zringnm  33994  rezh  34005  qqh0  34020  qqh1  34021  qqhucn  34028  esumpinfval  34109  hashf2  34120  esumcvg  34122  br2base  34306  sxbrsigalem3  34309  dya2iocbrsiga  34312  dya2icobrsiga  34313  sxbrsigalem1  34322  sxbrsigalem2  34323  sxbrsigalem4  34324  sxbrsigalem5  34325  sxbrsiga  34327  ballotlem2  34526  ballotlem4  34536  ballotlemi1  34540  ballotth  34575  signstf  34603  itgexpif  34643  chtvalz  34666  hgt750lemd  34685  hgt750lem  34688  tgoldbachgnn  34696  lfuhgr2  35146  subfacp1lem1  35206  subfacp1lem6  35212  kur14lem6  35238  cvmliftlem4  35315  satf0suc  35403  problem4  35695  quad3  35697  iexpire  35757  fununiq  35791  fvtransport  36055  bj-minftyccb  37248  taupilem2  37345  iccioo01  37350  1oequni2o  37391  finxp1o  37415  finxpreclem4  37417  cos2h  37640  tan2h  37641  poimirlem9  37658  poimirlem27  37676  poimirlem28  37677  ismblfin  37690  mbfposadd  37696  ftc1anclem5  37726  asindmre  37732  dvasin  37733  dvacos  37734  rrnval  37856  dihjatcclem4  41445  lcmineqlem12  42058  fisdomnn  42262  subex  42265  absex  42266  cjex  42267  cxpi11d  42361  redvmptabs  42378  readvrec  42380  sn-00idlem2  42417  sn-00id  42419  remul02  42423  rabren3dioph  42813  jm2.27dlem2  43009  rmydioph  43013  rmxdioph  43015  expdiophlem2  43021  expdioph  43022  arearect  43214  areaquad  43215  2omomeqom  43302  omnord1ex  43303  corclrcl  43706  iunrelexpuztr  43718  corcltrcl  43738  dffrege76  43938  k0004val0  44153  lhe4.4ex1a  44328  binomcxplemdvbinom  44352  binomcxplemnotnn0  44355  ax6e2ndeqALT  44930  sineq0ALT  44936  nregmodelf1o  45015  pnfel0pnf  45537  lptioo2cn  45654  limsup10ex  45782  liminf10ex  45783  icccncfext  45896  itgsin0pilem1  45959  itgsbtaddcnst  45991  stoweidlem13  46022  wallispilem2  46075  wallispilem4  46077  wallispi2lem1  46080  stirlinglem13  46095  dirkerper  46105  dirkertrigeqlem3  46109  dirkeritg  46111  dirkercncflem1  46112  dirkercncflem4  46115  fourierdlem42  46158  fourierdlem62  46177  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem114  46229  sqwvfoura  46237  fourierswlem  46239  fouriersw  46240  smfmullem4  46803  ceil5half3  47349  fmtnoprmfac2lem1  47560  fmtno4prm  47569  3exp4mod41  47610  41prothprmlem2  47612  6gbe  47765  7gbow  47766  8gbe  47767  9gbo  47768  11gbo  47769  sbgoldbalt  47775  nnsum4primesevenALTV  47795  usgrexmpl2nb0  48015  usgrexmpl2nb3  48018  gpg3nbgrvtx0  48058  gpg3nbgrvtx0ALT  48059  gpg3nbgrvtx1  48060  gpg5grlic  48073  0nodd  48125  oddinmgm  48130  2zrng0  48199  zlmodzxz0  48311  zlmodzxzequa  48452  zlmodzxzequap  48455  zlmodzxzldeplem3  48458  nnlog2ge0lt1  48526  blen1  48544  blen2  48545  nnolog2flm1  48550  ackval42  48656  ehl2eudisval0  48685  line2ylem  48711  i0oii  48874  io1ii  48875  sepfsepc  48882  rescofuf  49036  setc1ohomfval  49358  setc1ocofval  49359