Theorem mp3an 1458

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  raltp  4705  rextp  4706  opthhausdorff  5513  funopg  6581  feq12i  6709  ftp  7160  caovass  7615  caovdi  7634  ordom  7874  mptexw  7950  ofmres  7982  sbcoteq1a  8049  mpoexw  8077  xpord3lem  8148  omopthlem1  8673  omopthlem2  8674  omopthi  8675  on2recsfn  8681  xpcomen  9079  snnen2o  9253  unfilem3  9328  hartogs  9559  card2on  9569  unwf  9825  inlresf1  9930  inrresf1  9932  tskwe  9965  alephsmo  10117  dfac4  10137  dfac2a  10144  ackbij1lem13  10247  axdc2lem  10463  axcclem  10472  ondomon  10578  cfpwsdom  10599  pwfseqlem2  10674  pwfseqlem3  10675  1lt2pi  10920  addassi  11246  mulassi  11247  adddii  11248  adddiri  11249  lttri  11362  lelttri  11363  ltletri  11364  letri  11365  ltadd2i  11367  mul02lem2  11413  addrid  11416  addcani  11429  addcan2i  11430  mul12i  11431  mul32i  11432  add12i  11458  add32i  11459  subaddi  11569  subadd2i  11570  subsub23i  11572  addsubassi  11573  addsubi  11574  subcani  11575  subcan2i  11576  pnncani  11577  subdii  11685  subdiri  11686  ltadd1i  11790  leadd1i  11791  leadd2i  11792  ltsubaddi  11793  lesubaddi  11794  ltsubadd2i  11795  lesubadd2i  11796  ltaddsubi  11797  mulcani  11875  div23i  11994  div11i  11995  1mhlfehlf  12453  halfpm6th  12455  3halfnz  12663  mpoaddex  12994  addex  12995  mpomulex  12996  mulex  12997  unirnioo  13450  ioorebas  13452  xnn0xrge0  13507  fldiv4lem1div2  13826  uzenom  13953  nnenom  13969  seqexw  14006  m1expcl2  14074  i4  14191  expnass  14195  faclbnd4lem1  14276  bcn1  14296  hashfxnn0  14320  ccat2s1p1  14603  ccat2s1p2  14604  cats1fvn  14833  cats1fv  14834  cats1cat  14836  cats2cat  14837  wrdlen3s3  14924  abs3difi  15380  0.999...  15851  bpoly3  16026  ef01bndlem  16152  cos1bnd  16155  cos2bnd  16156  sin4lt0  16163  rpnnen2lem3  16184  rpnnen2lem11  16192  rpnnen  16195  rexpen  16196  aleph1irr  16214  3dvdsdec  16300  3dvds2dec  16301  divalglem2  16363  ndvdsi  16380  flodddiv4  16381  gcdaddmlem  16490  bezout  16510  3lcm2e6woprm  16577  6lcm4e12  16578  lcmf0  16596  lcmf2a3a4e12  16609  dec2dvds  17023  modxai  17028  modsubi  17032  gcdi  17033  numexp2x  17039  2exp5  17046  2exp11  17050  0symgefmndeq  19339  pmtrprfval  19433  m1expaddsub  19444  0frgp  19725  staffval  20716  cnfldcj  21275  cnfldds  21278  cnfldfunALT  21281  cnfldcjOLD  21288  cnflddsOLD  21291  cnfldfunALTOLD  21294  cnfldfunALTOLDOLD  21295  xrsadd  21299  xrsmul  21300  xrsds  21329  cnmgpid  21349  nn0srg  21357  rge0srg  21358  zring0  21371  pzriprnglem13  21406  pzriprng1ALT  21409  fermltlchr  21446  cnmsgnsubg  21496  psgninv  21501  re0g  21531  ocvfval  21585  frlmbas  21676  mdetrlin  22491  mdetunilem9  22509  leordtval2  23103  iscnp2  23130  utop3cls  24143  nmfval  24484  nmoffn  24615  nmofval  24618  icccld  24670  addcnlem  24767  iimulcn  24848  iimulcnOLD  24849  icopnfhmeo  24855  iccpnfcnv  24856  iccpnfhmeo  24857  xrhmeo  24858  xrhmph  24859  oprpiece1res1  24863  oprpiece1res2  24864  ishtpy  24885  pcoass  24938  cnstrcvs  25055  cncvs  25059  recvs  25060  recvsOLD  25061  qcvs  25062  zclmncvs  25063  tcphex  25132  cnfldcusp  25272  resscdrg  25273  reust  25296  recusp  25297  vitalilem4  25527  vitalilem5  25528  mbfdm  25542  dveflem  25898  dvlipcn  25914  c1lip2  25918  dgrid  26186  iaa  26247  abelthlem3  26357  abelthlem5  26359  abelth  26365  efcn  26367  sinhalfpilem  26385  sincosq1lem  26419  sincosq4sgn  26423  tangtx  26427  sincos4thpi  26435  sincos6thpi  26437  pigt3  26439  pige3ALT  26441  cos0pilt1  26453  logi  26508  relogcn  26559  dvlog2lem  26573  dvlog2  26574  logtayl  26581  logtayl2  26583  cxpsqrtlem  26623  cxpsqrt  26624  2irrexpq  26652  cxpcn2  26668  cxpcn3  26670  logblog  26711  2logb9irr  26714  2logb3irr  26716  2logb9irrALT  26717  sqrt2cxp2logb9e3  26718  2irrexpqALT  26719  ang180lem1  26728  ang180lem2  26729  1cubrlem  26760  mcubic  26766  quart1lem  26774  quart1  26775  reasinsin  26815  atancj  26829  efiatan  26831  atantan  26842  atanbndlem  26844  atan1  26847  atancn  26855  atantayl2  26857  log2cnv  26863  log2tlbnd  26864  log2ublem1  26865  log2ublem2  26866  log2ub  26868  efrlim  26888  efrlimOLD  26889  scvxcvx  26905  1sgm2ppw  27120  ppiub  27124  bclbnd  27200  bposlem8  27211  lgsdir2lem1  27245  lgsdir2lem5  27249  lgseisenlem1  27295  lgseisenlem2  27296  lgsquadlem1  27300  chebbnd1  27392  dchrvmasumlem2  27418  norecfn  27850  norec2fn  27860  addsproplem2  27874  addsproplem6  27878  negsproplem2  27928  mulsproplem2  28004  mulsproplem3  28005  mulsproplem5  28007  mulsproplem6  28008  mulsproplem7  28009  mulsproplem8  28010  mulsproplem13  28015  mulsproplem14  28016  istrkg3ld  28252  trgcgrg  28306  ax5seglem7  28733  axlowdimlem6  28745  axlowdimlem8  28747  axlowdimlem11  28750  elntg2  28783  cusgrsizeindb1  29251  vtxdginducedm1  29344  0grrusgr  29380  erclwwlktr  29819  erclwwlkntr  29868  wlk2v2e  29954  upgr3v3e3cycl  29977  konigsberglem1  30049  konigsberglem2  30050  konigsberglem3  30051  konigsberglem5  30053  ex-fl  30244  ex-mod  30246  ex-hash  30250  ex-lcm  30255  0vfval  30403  smcnlem  30494  lnocoi  30554  nmlno0lem  30590  nmblolbii  30596  blocnilem  30601  blocni  30602  cncph  30616  isph  30619  ip0i  30622  ip1ilem  30623  ip2i  30625  ipdirilem  30626  ipasslem7  30633  ipasslem8  30634  ipasslem9  30635  ipasslem10  30636  ipasslem11  30637  ip2dii  30641  pythi  30647  siilem1  30648  siilem2  30649  siii  30650  hvmulassi  30843  hvmulcomi  30844  hvdistr1i  30848  hvsubdistr1i  30849  hvassi  30850  hvadd32i  30851  hvsubassi  30852  hvsub32i  30853  normlem0  30906  normlem8  30914  normlem9  30915  bcseqi  30917  polid2i  30954  hhph  30975  hlim0  31032  shscli  31114  shlessi  31174  shlej1i  31175  omlsilem  31199  shlubi  31212  h1de2i  31350  pjadjii  31471  pjaddii  31472  pjmulii  31474  pjdifnormii  31480  pjcji  31481  hoaddsubassi  31617  eigrei  31631  eigposi  31633  eigorthi  31634  adj0  31791  lnopeq0lem1  31802  lnopunilem1  31807  lnophmlem2  31814  nmcexi  31823  nmcopexi  31824  lnfn0i  31839  nmcfnexi  31848  mdexchi  32132  xppreima2  32420  dp2clq  32586  dp2lt  32590  dp2ltc  32592  dpexpp1  32613  dpmul  32618  dpmul4  32619  elxrge02  32637  xrge0adddir  32730  psgnid  32796  cnmsgn0g  32845  altgnsg  32848  xrnarchi  32870  xrge0slmod  33000  znfermltl  33018  ccfldextdgrr  33292  raddcn  33466  xrge0iifcnv  33470  xrge0iifiso  33472  xrge0iifhmeo  33473  xrge0iifhom  33474  xrge0iifmhm  33476  xrge0mulc1cn  33478  lmlimxrge0  33485  pnfneige0  33488  lmxrge0  33489  zringnm  33495  rezh  33508  qqh0  33521  qqh1  33522  qqhucn  33529  esumpinfval  33628  hashf2  33639  esumcvg  33641  br2base  33825  sxbrsigalem3  33828  dya2iocbrsiga  33831  dya2icobrsiga  33832  sxbrsigalem1  33841  sxbrsigalem2  33842  sxbrsigalem4  33843  sxbrsigalem5  33844  sxbrsiga  33846  ballotlem2  34044  ballotlem4  34054  ballotlemi1  34058  ballotth  34093  sgnclre  34095  signstf  34134  itgexpif  34174  chtvalz  34197  hgt750lemd  34216  hgt750lem  34219  tgoldbachgnn  34227  lfuhgr2  34664  subfacp1lem1  34725  subfacp1lem6  34731  kur14lem6  34757  cvmliftlem4  34834  satf0suc  34922  problem4  35208  quad3  35210  iexpire  35265  fununiq  35300  fvtransport  35564  bj-minftyccb  36640  taupilem2  36737  iccioo01  36742  1oequni2o  36783  finxp1o  36807  finxpreclem4  36809  cos2h  37019  tan2h  37020  poimirlem9  37037  poimirlem27  37055  poimirlem28  37056  ismblfin  37069  mbfposadd  37075  ftc1anclem5  37105  asindmre  37111  dvasin  37112  dvacos  37113  rrnval  37235  el3v  37626  dihjatcclem4  40831  lcmineqlem12  41448  cxpi11d  41836  sn-00idlem2  41876  sn-00id  41878  remul02  41882  rabren3dioph  42157  jm2.27dlem2  42353  rmydioph  42357  rmxdioph  42359  expdiophlem2  42365  expdioph  42366  arearect  42566  areaquad  42567  2omomeqom  42655  omnord1ex  42656  corclrcl  43060  iunrelexpuztr  43072  corcltrcl  43092  dffrege76  43292  k0004val0  43507  lhe4.4ex1a  43689  binomcxplemdvbinom  43713  binomcxplemnotnn0  43716  ax6e2ndeqALT  44293  sineq0ALT  44299  pnfel0pnf  44836  lptioo2cn  44956  limsup10ex  45084  liminf10ex  45085  icccncfext  45198  itgsin0pilem1  45261  itgsbtaddcnst  45293  stoweidlem13  45324  wallispilem2  45377  wallispilem4  45379  wallispi2lem1  45382  stirlinglem13  45397  dirkerper  45407  dirkertrigeqlem3  45411  dirkeritg  45413  dirkercncflem1  45414  dirkercncflem4  45417  fourierdlem42  45460  fourierdlem62  45479  fourierdlem102  45519  fourierdlem103  45520  fourierdlem104  45521  fourierdlem114  45531  sqwvfoura  45539  fourierswlem  45541  fouriersw  45542  smfmullem4  46105  fmtnoprmfac2lem1  46829  fmtno4prm  46838  3exp4mod41  46879  41prothprmlem2  46881  6gbe  47034  7gbow  47035  8gbe  47036  9gbo  47037  11gbo  47038  sbgoldbalt  47044  nnsum4primesevenALTV  47064  0nodd  47155  oddinmgm  47160  2zrng0  47229  zlmodzxz0  47343  zlmodzxzequa  47487  zlmodzxzequap  47490  zlmodzxzldeplem3  47493  nnlog2ge0lt1  47562  blen1  47580  blen2  47581  nnolog2flm1  47586  ackval42  47692  ehl2eudisval0  47721  line2ylem  47747  i0oii  47861  io1ii  47862  sepfsepc  47869