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  3449  raltp  4663  rextp  4664  opthhausdorff  5466  funopg  6527  feq12i  6656  ftp  7104  caovass  7560  caovdi  7579  ordom  7820  mptexw  7899  ofmres  7930  sbcoteq1a  7997  mpoexw  8024  xpord3lem  8093  omopthlem1  8589  omopthlem2  8590  omopthi  8591  on2recsfn  8597  xpcomen  9000  snnen2o  9149  unfilem3  9211  hartogs  9453  card2on  9463  unwf  9726  inlresf1  9831  inrresf1  9833  tskwe  9866  alephsmo  10016  dfac4  10036  dfac2a  10044  ackbij1lem13  10145  axdc2lem  10362  axcclem  10371  ondomon  10477  cfpwsdom  10499  pwfseqlem2  10574  pwfseqlem3  10575  1lt2pi  10820  addassi  11146  mulassi  11147  adddii  11148  adddiri  11149  lttri  11263  lelttri  11264  ltletri  11265  letri  11266  ltadd2i  11268  mul02lem2  11314  addrid  11317  addcani  11330  addcan2i  11331  mul12i  11332  mul32i  11333  add12i  11360  add32i  11361  subaddi  11472  subadd2i  11473  subsub23i  11475  addsubassi  11476  addsubi  11477  subcani  11478  subcan2i  11479  pnncani  11480  subdii  11590  subdiri  11591  ltadd1i  11695  leadd1i  11696  leadd2i  11697  ltsubaddi  11698  lesubaddi  11699  ltsubadd2i  11700  lesubadd2i  11701  ltaddsubi  11702  mulcani  11780  div23i  11903  div11i  11904  3halfnz  12575  mpoaddex  12905  addex  12906  mpomulex  12907  mulex  12908  unirnioo  13369  ioorebas  13371  xnn0xrge0  13426  fldiv4lem1div2  13761  uzenom  13891  nnenom  13907  seqexw  13944  m1expcl2  14012  i4  14131  expnass  14135  faclbnd4lem1  14220  bcn1  14240  hashfxnn0  14264  ccat2s1p1  14557  ccat2s1p2  14558  cats1fvn  14785  cats1fv  14786  cats1cat  14788  cats2cat  14789  wrdlen3s3  14876  abs3difi  15337  0.999...  15808  bpoly3  15985  ef01bndlem  16113  cos1bnd  16116  cos2bnd  16117  sin4lt0  16124  rpnnen2lem3  16145  rpnnen2lem11  16153  rpnnen  16156  rexpen  16157  aleph1irr  16175  3dvdsdec  16263  3dvds2dec  16264  divalglem2  16326  ndvdsi  16343  flodddiv4  16346  gcdaddmlem  16455  bezout  16474  3lcm2e6woprm  16546  6lcm4e12  16547  lcmf0  16565  lcmf2a3a4e12  16578  dec2dvds  16995  modxai  17000  modsubi  17004  gcdi  17005  numexp2x  17010  2exp5  17017  2exp11  17021  ex-chn2  18565  0symgefmndeq  19327  pmtrprfval  19420  m1expaddsub  19431  0frgp  19712  staffval  20778  cnfldcj  21322  cnfldds  21325  cnfldfunALT  21328  cnfldcjOLD  21335  cnflddsOLD  21338  cnfldfunALTOLD  21341  xrsadd  21344  xrsmul  21345  xrsds  21368  cnmgpid  21388  nn0srg  21396  rge0srg  21397  zring0  21417  pzriprnglem13  21452  pzriprng1ALT  21455  fermltlchr  21488  cnmsgnsubg  21536  psgninv  21541  re0g  21571  ocvfval  21625  frlmbas  21714  mdetrlin  22550  mdetunilem9  22568  leordtval2  23160  iscnp2  23187  utop3cls  24199  nmfval  24536  nmoffn  24659  nmofval  24662  icccld  24714  addcnlem  24813  iimulcn  24894  iimulcnOLD  24895  icopnfhmeo  24901  iccpnfcnv  24902  iccpnfhmeo  24903  xrhmeo  24904  xrhmph  24905  oprpiece1res1  24909  oprpiece1res2  24910  ishtpy  24931  pcoass  24984  cnstrcvs  25101  cncvs  25105  recvs  25106  qcvs  25107  zclmncvs  25108  tcphex  25177  cnfldcusp  25317  resscdrg  25318  reust  25341  recusp  25342  vitalilem4  25572  vitalilem5  25573  mbfdm  25587  dveflem  25943  dvlipcn  25959  c1lip2  25963  dgrid  26230  iaa  26293  abelthlem3  26403  abelthlem5  26405  abelth  26411  efcn  26413  sinhalfpilem  26432  sincosq1lem  26466  sincosq4sgn  26470  tangtx  26474  sincos4thpi  26482  sincos6thpi  26485  pigt3  26487  pige3ALT  26489  cos0pilt1  26501  logi  26556  relogcn  26607  dvlog2lem  26621  dvlog2  26622  logtayl  26629  logtayl2  26631  cxpsqrtlem  26671  cxpsqrt  26672  2irrexpq  26700  cxpcn2  26716  cxpcn3  26718  logblog  26762  2logb9irr  26765  2logb3irr  26767  2logb9irrALT  26768  sqrt2cxp2logb9e3  26769  2irrexpqALT  26770  ang180lem1  26779  ang180lem2  26780  1cubrlem  26811  mcubic  26817  quart1lem  26825  quart1  26826  reasinsin  26866  atancj  26880  efiatan  26882  atantan  26893  atanbndlem  26895  atan1  26898  atancn  26906  atantayl2  26908  log2cnv  26914  log2tlbnd  26915  log2ublem1  26916  log2ublem2  26917  log2ub  26919  efrlim  26939  efrlimOLD  26940  scvxcvx  26956  1sgm2ppw  27171  ppiub  27175  bclbnd  27251  bposlem8  27262  lgsdir2lem1  27296  lgsdir2lem5  27300  lgseisenlem1  27346  lgseisenlem2  27347  lgsquadlem1  27351  chebbnd1  27443  dchrvmasumlem2  27469  norecfn  27946  norec2fn  27956  addsproplem2  27970  addsproplem6  27974  addbdaylem  28017  neg1s  28027  negsproplem2  28029  mulsproplem2  28117  mulsproplem3  28118  mulsproplem5  28120  mulsproplem6  28121  mulsproplem7  28122  mulsproplem8  28123  mulsproplem13  28128  mulsproplem14  28129  0zs  28388  zseo  28422  twocut  28423  bdaypw2n0bndlem  28463  bdaypw2bnd  28465  bdayfinbndlem1  28467  z12bdaylem2  28471  istrkg3ld  28537  trgcgrg  28591  ax5seglem7  29012  axlowdimlem6  29024  axlowdimlem8  29026  axlowdimlem11  29029  elntg2  29062  cusgrsizeindb1  29528  vtxdginducedm1  29621  0grrusgr  29657  erclwwlktr  30101  erclwwlkntr  30150  wlk2v2e  30236  upgr3v3e3cycl  30259  konigsberglem1  30331  konigsberglem2  30332  konigsberglem3  30333  konigsberglem5  30335  ex-fl  30526  ex-mod  30528  ex-hash  30532  ex-lcm  30537  0vfval  30685  smcnlem  30776  lnocoi  30836  nmlno0lem  30872  nmblolbii  30878  blocnilem  30883  blocni  30884  cncph  30898  isph  30901  ip0i  30904  ip1ilem  30905  ip2i  30907  ipdirilem  30908  ipasslem7  30915  ipasslem8  30916  ipasslem9  30917  ipasslem10  30918  ipasslem11  30919  ip2dii  30923  pythi  30929  siilem1  30930  siilem2  30931  siii  30932  hvmulassi  31125  hvmulcomi  31126  hvdistr1i  31130  hvsubdistr1i  31131  hvassi  31132  hvadd32i  31133  hvsubassi  31134  hvsub32i  31135  normlem0  31188  normlem8  31196  normlem9  31197  bcseqi  31199  polid2i  31236  hhph  31257  hlim0  31314  shscli  31396  shlessi  31456  shlej1i  31457  omlsilem  31481  shlubi  31494  h1de2i  31632  pjadjii  31753  pjaddii  31754  pjmulii  31756  pjdifnormii  31762  pjcji  31763  hoaddsubassi  31899  eigrei  31913  eigposi  31915  eigorthi  31916  adj0  32073  lnopeq0lem1  32084  lnopunilem1  32089  lnophmlem2  32096  nmcexi  32105  nmcopexi  32106  lnfn0i  32121  nmcfnexi  32130  mdexchi  32414  xppreima2  32732  sgnclre  32915  dp2clq  32964  dp2lt  32968  dp2ltc  32970  dpexpp1  32991  dpmul  32996  dpmul4  32997  elxrge02  33015  xrge0adddir  33102  psgnid  33181  cnmsgn0g  33230  altgnsg  33233  xrnarchi  33268  xrge0slmod  33431  znfermltl  33449  ccfldextdgrr  33831  cos9thpiminplylem4  33944  cos9thpiminplylem5  33945  raddcn  34088  xrge0iifcnv  34092  xrge0iifiso  34094  xrge0iifhmeo  34095  xrge0iifhom  34096  xrge0iifmhm  34098  xrge0mulc1cn  34100  lmlimxrge0  34107  pnfneige0  34110  lmxrge0  34111  zringnm  34117  rezh  34128  qqh0  34143  qqh1  34144  qqhucn  34151  esumpinfval  34232  hashf2  34243  esumcvg  34245  br2base  34428  sxbrsigalem3  34431  dya2iocbrsiga  34434  dya2icobrsiga  34435  sxbrsigalem1  34444  sxbrsigalem2  34445  sxbrsigalem4  34446  sxbrsigalem5  34447  sxbrsiga  34449  ballotlem2  34648  ballotlem4  34658  ballotlemi1  34662  ballotth  34697  signstf  34725  itgexpif  34765  chtvalz  34788  hgt750lemd  34807  hgt750lem  34810  tgoldbachgnn  34818  lfuhgr2  35315  subfacp1lem1  35375  subfacp1lem6  35381  kur14lem6  35407  cvmliftlem4  35484  satf0suc  35572  problem4  35864  quad3  35866  iexpire  35931  fununiq  35965  fvtransport  36228  bj-minftyccb  37432  taupilem2  37529  iccioo01  37534  1oequni2o  37575  finxp1o  37599  finxpreclem4  37601  cos2h  37814  tan2h  37815  poimirlem9  37832  poimirlem27  37850  poimirlem28  37851  ismblfin  37864  mbfposadd  37870  ftc1anclem5  37900  asindmre  37906  dvasin  37907  dvacos  37908  rrnval  38030  dihjatcclem4  41749  lcmineqlem12  42362  fisdomnn  42566  subex  42569  absex  42570  cjex  42571  cxpi11d  42665  redvmptabs  42682  readvrec  42684  sn-00idlem2  42721  sn-00id  42723  remul02  42727  rabren3dioph  43124  jm2.27dlem2  43319  rmydioph  43323  rmxdioph  43325  expdiophlem2  43331  expdioph  43332  arearect  43524  areaquad  43525  2omomeqom  43612  omnord1ex  43613  corclrcl  44015  iunrelexpuztr  44027  corcltrcl  44047  dffrege76  44247  k0004val0  44462  lhe4.4ex1a  44637  binomcxplemdvbinom  44661  binomcxplemnotnn0  44664  ax6e2ndeqALT  45238  sineq0ALT  45244  nregmodelf1o  45323  pnfel0pnf  45841  lptioo2cn  45956  limsup10ex  46084  liminf10ex  46085  icccncfext  46198  itgsin0pilem1  46261  itgsbtaddcnst  46293  stoweidlem13  46324  wallispilem2  46377  wallispilem4  46379  wallispi2lem1  46382  stirlinglem13  46397  dirkerper  46407  dirkertrigeqlem3  46411  dirkeritg  46413  dirkercncflem1  46414  dirkercncflem4  46417  fourierdlem42  46460  fourierdlem62  46479  fourierdlem102  46519  fourierdlem103  46520  fourierdlem104  46521  fourierdlem114  46531  sqwvfoura  46539  fourierswlem  46541  fouriersw  46542  smfmullem4  47105  nthrucw  47197  ceil5half3  47653  8mod5e3  47673  fmtnoprmfac2lem1  47879  fmtno4prm  47888  3exp4mod41  47929  41prothprmlem2  47931  6gbe  48084  7gbow  48085  8gbe  48086  9gbo  48087  11gbo  48088  sbgoldbalt  48094  nnsum4primesevenALTV  48114  usgrexmpl2nb0  48344  usgrexmpl2nb3  48347  gpg3nbgrvtx0  48389  gpg3nbgrvtx0ALT  48390  gpg3nbgrvtx1  48391  gpg5grlim  48406  gpg5grlic  48407  0nodd  48483  oddinmgm  48488  2zrng0  48557  zlmodzxz0  48669  zlmodzxzequa  48809  zlmodzxzequap  48812  zlmodzxzldeplem3  48815  nnlog2ge0lt1  48879  blen1  48897  blen2  48898  nnolog2flm1  48903  ackval42  49009  ehl2eudisval0  49038  line2ylem  49064  i0oii  49232  io1ii  49233  sepfsepc  49240  rescofuf  49405  setc1ohomfval  49805  setc1ocofval  49806