Theorem mp3an 1457

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  raltp  4644  rextp  4645  opthhausdorff  5410  funopg  6392  feq12i  6510  ftp  6922  caovass  7351  caovdi  7370  ordom  7592  mptexw  7657  ofmres  7688  mpoexw  7779  omopthlem1  8285  omopthlem2  8286  omopthi  8287  xpcomen  8611  unfilem3  8787  hartogs  9011  card2on  9021  unwf  9242  inlresf1  9347  inrresf1  9349  tskwe  9382  alephsmo  9531  dfac4  9551  dfac2a  9558  ackbij1lem13  9657  axdc2lem  9873  axcclem  9882  ondomon  9988  cfpwsdom  10009  pwfseqlem2  10084  pwfseqlem3  10085  1lt2pi  10330  addassi  10654  mulassi  10655  adddii  10656  adddiri  10657  lttri  10769  lelttri  10770  ltletri  10771  letri  10772  ltadd2i  10774  mul02lem2  10820  addid1  10823  addcani  10836  addcan2i  10837  mul12i  10838  mul32i  10839  add12i  10865  add32i  10866  subaddi  10976  subadd2i  10977  subsub23i  10979  addsubassi  10980  addsubi  10981  subcani  10982  subcan2i  10983  pnncani  10984  subdii  11092  subdiri  11093  ltadd1i  11197  leadd1i  11198  leadd2i  11199  ltsubaddi  11200  lesubaddi  11201  ltsubadd2i  11202  lesubadd2i  11203  ltaddsubi  11204  mulcani  11282  div23i  11401  div11i  11402  1mhlfehlf  11859  halfpm6th  11861  3halfnz  12064  addex  12390  mulex  12391  unirnioo  12840  ioorebas  12842  xnn0xrge0  12894  fldiv4lem1div2  13210  uzenom  13335  nnenom  13351  seqexw  13388  m1expcl2  13454  i4  13570  expnass  13573  faclbnd4lem1  13656  bcn1  13676  hashfxnn0  13700  ccat2s1p1  13988  ccat2s1p2  13989  cats1fvn  14223  cats1fv  14224  cats1cat  14226  cats2cat  14227  wrdlen3s3  14314  abs3difi  14772  0.999...  15240  bpoly3  15415  ef01bndlem  15540  cos1bnd  15543  cos2bnd  15544  sin4lt0  15551  rpnnen2lem3  15572  rpnnen2lem11  15580  rpnnen  15583  rexpen  15584  aleph1irr  15602  3dvdsdec  15684  3dvds2dec  15685  divalglem2  15749  ndvdsi  15766  flodddiv4  15767  gcdaddmlem  15875  bezout  15894  3lcm2e6woprm  15962  6lcm4e12  15963  lcmf0  15981  lcmf2a3a4e12  15994  dec2dvds  16402  modxai  16407  modsubi  16411  gcdi  16412  numexp2x  16418  prdsval  16731  prdsds  16740  0symgefmndeq  18525  pmtrprfval  18618  m1expaddsub  18629  0frgp  18908  staffval  19621  cnfldcj  20555  cnfldds  20558  cnfldfun  20560  xrsadd  20565  xrsmul  20566  xrsds  20591  cnmgpid  20610  nn0srg  20618  rge0srg  20619  zring0  20630  cnmsgnsubg  20724  psgninv  20729  re0g  20759  ocvfval  20813  frlmbas  20902  mdetrlin  21214  mdetunilem9  21232  leordtval2  21823  iscnp2  21850  utop3cls  22863  nmfval  23201  nmoffn  23323  nmofval  23326  icccld  23378  addcnlem  23475  iimulcn  23545  icopnfhmeo  23550  iccpnfcnv  23551  iccpnfhmeo  23552  xrhmeo  23553  xrhmph  23554  oprpiece1res1  23558  oprpiece1res2  23559  ishtpy  23579  pcoass  23631  cnstrcvs  23748  cncvs  23752  recvs  23753  qcvs  23754  zclmncvs  23755  tcphex  23823  cnfldcusp  23963  resscdrg  23964  reust  23987  recusp  23988  vitalilem4  24215  vitalilem5  24216  mbfdm  24230  dveflem  24579  dvlipcn  24594  c1lip2  24598  dgrid  24857  iaa  24917  abelthlem3  25024  abelthlem5  25026  abelth  25032  efcn  25034  sinhalfpilem  25052  sincosq1lem  25086  sincosq4sgn  25090  tangtx  25094  sincos4thpi  25102  sincos6thpi  25104  pigt3  25106  pige3ALT  25108  relogcn  25224  dvlog2lem  25238  dvlog2  25239  logtayl  25246  logtayl2  25248  cxpsqrtlem  25288  cxpsqrt  25289  2irrexpq  25316  cxpcn2  25330  cxpcn3  25332  logblog  25373  2logb9irr  25376  2logb3irr  25378  2logb9irrALT  25379  sqrt2cxp2logb9e3  25380  2irrexpqALT  25381  ang180lem1  25390  ang180lem2  25391  1cubrlem  25422  mcubic  25428  quart1lem  25436  quart1  25437  reasinsin  25477  atancj  25491  efiatan  25493  atantan  25504  atanbndlem  25506  atan1  25509  atancn  25517  atantayl2  25519  log2cnv  25525  log2tlbnd  25526  log2ublem1  25527  log2ublem2  25528  log2ub  25530  efrlim  25550  scvxcvx  25566  1sgm2ppw  25779  ppiub  25783  bclbnd  25859  bposlem8  25870  lgsdir2lem1  25904  lgsdir2lem5  25908  lgseisenlem1  25954  lgseisenlem2  25955  lgsquadlem1  25959  chebbnd1  26051  dchrvmasumlem2  26077  istrkg3ld  26250  trgcgrg  26304  ax5seglem7  26724  axlowdimlem6  26736  axlowdimlem8  26738  axlowdimlem11  26741  elntg2  26774  cusgrsizeindb1  27235  vtxdginducedm1  27328  0grrusgr  27364  erclwwlktr  27803  erclwwlkntr  27853  wlk2v2e  27939  upgr3v3e3cycl  27962  konigsberglem1  28034  konigsberglem2  28035  konigsberglem3  28036  konigsberglem5  28038  ex-fl  28229  ex-mod  28231  ex-hash  28235  ex-lcm  28240  0vfval  28386  smcnlem  28477  lnocoi  28537  nmlno0lem  28573  nmblolbii  28579  blocnilem  28584  blocni  28585  cncph  28599  isph  28602  ip0i  28605  ip1ilem  28606  ip2i  28608  ipdirilem  28609  ipasslem7  28616  ipasslem8  28617  ipasslem9  28618  ipasslem10  28619  ipasslem11  28620  ip2dii  28624  pythi  28630  siilem1  28631  siilem2  28632  siii  28633  hvmulassi  28826  hvmulcomi  28827  hvdistr1i  28831  hvsubdistr1i  28832  hvassi  28833  hvadd32i  28834  hvsubassi  28835  hvsub32i  28836  normlem0  28889  normlem8  28897  normlem9  28898  bcseqi  28900  polid2i  28937  hhph  28958  hlim0  29015  shscli  29097  shlessi  29157  shlej1i  29158  omlsilem  29182  shlubi  29195  h1de2i  29333  pjadjii  29454  pjaddii  29455  pjmulii  29457  pjdifnormii  29463  pjcji  29464  hoaddsubassi  29600  eigrei  29614  eigposi  29616  eigorthi  29617  adj0  29774  lnopeq0lem1  29785  lnopunilem1  29790  lnophmlem2  29797  nmcexi  29806  nmcopexi  29807  lnfn0i  29822  nmcfnexi  29831  mdexchi  30115  xppreima2  30398  dp2clq  30561  dp2lt  30565  dp2ltc  30567  dpexpp1  30588  dpmul  30593  dpmul4  30594  elxrge02  30612  xrge0adddir  30683  psgnid  30743  cnmsgn0g  30792  altgnsg  30795  xrnarchi  30817  xrge0slmod  30921  ccfldextdgrr  31061  raddcn  31176  xrge0iifcnv  31180  xrge0iifiso  31182  xrge0iifhmeo  31183  xrge0iifhom  31184  xrge0iifmhm  31186  xrge0mulc1cn  31188  lmlimxrge0  31195  pnfneige0  31198  lmxrge0  31199  zringnm  31205  rezh  31216  qqh0  31229  qqh1  31230  qqhucn  31237  esumpinfval  31336  hashf2  31347  esumcvg  31349  br2base  31531  sxbrsigalem3  31534  dya2iocbrsiga  31537  dya2icobrsiga  31538  sxbrsigalem1  31547  sxbrsigalem2  31548  sxbrsigalem4  31549  sxbrsigalem5  31550  sxbrsiga  31552  ballotlem2  31750  ballotlem4  31760  ballotlemi1  31764  ballotth  31799  sgnclre  31801  signstf  31840  itgexpif  31881  chtvalz  31904  hgt750lemd  31923  hgt750lem  31926  tgoldbachgnn  31934  lfuhgr2  32369  subfacp1lem1  32430  subfacp1lem6  32436  kur14lem6  32462  cvmliftlem4  32539  satf0suc  32627  problem4  32915  quad3  32917  logi  32970  iexpire  32971  fununiq  33016  fvtransport  33497  bj-minftyccb  34511  taupilem2  34607  1oequni2o  34653  finxp1o  34677  finxpreclem4  34679  cos2h  34887  tan2h  34888  poimirlem9  34905  poimirlem27  34923  poimirlem28  34924  ismblfin  34937  mbfposadd  34943  ftc1anclem5  34975  asindmre  34981  dvasin  34982  dvacos  34983  rrnval  35109  el3v  35495  dihjatcclem4  38561  sn-00idlem2  39235  sn-00id  39237  remul02  39241  sn-0lt1  39252  rabren3dioph  39418  jm2.27dlem2  39613  rmydioph  39617  rmxdioph  39619  expdiophlem2  39625  expdioph  39626  arearect  39828  areaquad  39829  corclrcl  40058  iunrelexpuztr  40070  corcltrcl  40090  dffrege76  40291  k0004val0  40510  lhe4.4ex1a  40667  binomcxplemdvbinom  40691  binomcxplemnotnn0  40694  ax6e2ndeqALT  41271  sineq0ALT  41277  pnfel0pnf  41810  lptioo2cn  41932  limsup10ex  42060  liminf10ex  42061  icccncfext  42176  itgsin0pilem1  42241  itgsbtaddcnst  42273  stoweidlem13  42305  wallispilem2  42358  wallispilem4  42360  wallispi2lem1  42363  stirlinglem13  42378  dirkerper  42388  dirkertrigeqlem3  42392  dirkeritg  42394  dirkercncflem1  42395  dirkercncflem4  42398  fourierdlem42  42441  fourierdlem62  42460  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem114  42512  sqwvfoura  42520  fourierswlem  42522  fouriersw  42523  smfmullem4  43076  fmtnoprmfac2lem1  43735  fmtno4prm  43744  2exp5  43762  2exp11  43772  3exp4mod41  43788  41prothprmlem2  43790  6gbe  43943  7gbow  43944  8gbe  43945  9gbo  43946  11gbo  43947  sbgoldbalt  43953  nnsum4primesevenALTV  43973  0nodd  44084  oddinmgm  44089  2zrng0  44216  zlmodzxz0  44411  zlmodzxzequa  44558  zlmodzxzequap  44561  zlmodzxzldeplem3  44564  nnlog2ge0lt1  44633  blen1  44651  blen2  44652  nnolog2flm1  44657  ehl2eudisval0  44719  line2ylem  44745