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  3441  raltp  4655  rextp  4656  opthhausdorff  5454  funopg  6510  feq12i  6639  ftp  7084  caovass  7540  caovdi  7559  ordom  7800  mptexw  7879  ofmres  7910  sbcoteq1a  7977  mpoexw  8004  xpord3lem  8073  omopthlem1  8568  omopthlem2  8569  omopthi  8570  on2recsfn  8576  xpcomen  8975  snnen2o  9123  unfilem3  9185  hartogs  9424  card2on  9434  unwf  9694  inlresf1  9799  inrresf1  9801  tskwe  9834  alephsmo  9984  dfac4  10004  dfac2a  10012  ackbij1lem13  10113  axdc2lem  10330  axcclem  10339  ondomon  10445  cfpwsdom  10466  pwfseqlem2  10541  pwfseqlem3  10542  1lt2pi  10787  addassi  11113  mulassi  11114  adddii  11115  adddiri  11116  lttri  11230  lelttri  11231  ltletri  11232  letri  11233  ltadd2i  11235  mul02lem2  11281  addrid  11284  addcani  11297  addcan2i  11298  mul12i  11299  mul32i  11300  add12i  11327  add32i  11328  subaddi  11439  subadd2i  11440  subsub23i  11442  addsubassi  11443  addsubi  11444  subcani  11445  subcan2i  11446  pnncani  11447  subdii  11557  subdiri  11558  ltadd1i  11662  leadd1i  11663  leadd2i  11664  ltsubaddi  11665  lesubaddi  11666  ltsubadd2i  11667  lesubadd2i  11668  ltaddsubi  11669  mulcani  11747  div23i  11870  div11i  11871  3halfnz  12543  mpoaddex  12877  addex  12878  mpomulex  12879  mulex  12880  unirnioo  13340  ioorebas  13342  xnn0xrge0  13397  fldiv4lem1div2  13729  uzenom  13859  nnenom  13875  seqexw  13912  m1expcl2  13980  i4  14099  expnass  14103  faclbnd4lem1  14188  bcn1  14208  hashfxnn0  14232  ccat2s1p1  14524  ccat2s1p2  14525  cats1fvn  14752  cats1fv  14753  cats1cat  14755  cats2cat  14756  wrdlen3s3  14843  abs3difi  15304  0.999...  15775  bpoly3  15952  ef01bndlem  16080  cos1bnd  16083  cos2bnd  16084  sin4lt0  16091  rpnnen2lem3  16112  rpnnen2lem11  16120  rpnnen  16123  rexpen  16124  aleph1irr  16142  3dvdsdec  16230  3dvds2dec  16231  divalglem2  16293  ndvdsi  16310  flodddiv4  16313  gcdaddmlem  16422  bezout  16441  3lcm2e6woprm  16513  6lcm4e12  16514  lcmf0  16532  lcmf2a3a4e12  16545  dec2dvds  16962  modxai  16967  modsubi  16971  gcdi  16972  numexp2x  16977  2exp5  16984  2exp11  16988  0symgefmndeq  19260  pmtrprfval  19353  m1expaddsub  19364  0frgp  19645  staffval  20710  cnfldcj  21254  cnfldds  21257  cnfldfunALT  21260  cnfldcjOLD  21267  cnflddsOLD  21270  cnfldfunALTOLD  21273  xrsadd  21276  xrsmul  21277  xrsds  21300  cnmgpid  21320  nn0srg  21328  rge0srg  21329  zring0  21349  pzriprnglem13  21384  pzriprng1ALT  21387  fermltlchr  21420  cnmsgnsubg  21468  psgninv  21473  re0g  21503  ocvfval  21557  frlmbas  21646  mdetrlin  22471  mdetunilem9  22489  leordtval2  23081  iscnp2  23108  utop3cls  24120  nmfval  24457  nmoffn  24580  nmofval  24583  icccld  24635  addcnlem  24734  iimulcn  24815  iimulcnOLD  24816  icopnfhmeo  24822  iccpnfcnv  24823  iccpnfhmeo  24824  xrhmeo  24825  xrhmph  24826  oprpiece1res1  24830  oprpiece1res2  24831  ishtpy  24852  pcoass  24905  cnstrcvs  25022  cncvs  25026  recvs  25027  qcvs  25028  zclmncvs  25029  tcphex  25098  cnfldcusp  25238  resscdrg  25239  reust  25262  recusp  25263  vitalilem4  25493  vitalilem5  25494  mbfdm  25508  dveflem  25864  dvlipcn  25880  c1lip2  25884  dgrid  26151  iaa  26214  abelthlem3  26324  abelthlem5  26326  abelth  26332  efcn  26334  sinhalfpilem  26353  sincosq1lem  26387  sincosq4sgn  26391  tangtx  26395  sincos4thpi  26403  sincos6thpi  26406  pigt3  26408  pige3ALT  26410  cos0pilt1  26422  logi  26477  relogcn  26528  dvlog2lem  26542  dvlog2  26543  logtayl  26550  logtayl2  26552  cxpsqrtlem  26592  cxpsqrt  26593  2irrexpq  26621  cxpcn2  26637  cxpcn3  26639  logblog  26683  2logb9irr  26686  2logb3irr  26688  2logb9irrALT  26689  sqrt2cxp2logb9e3  26690  2irrexpqALT  26691  ang180lem1  26700  ang180lem2  26701  1cubrlem  26732  mcubic  26738  quart1lem  26746  quart1  26747  reasinsin  26787  atancj  26801  efiatan  26803  atantan  26814  atanbndlem  26816  atan1  26819  atancn  26827  atantayl2  26829  log2cnv  26835  log2tlbnd  26836  log2ublem1  26837  log2ublem2  26838  log2ub  26840  efrlim  26860  efrlimOLD  26861  scvxcvx  26877  1sgm2ppw  27092  ppiub  27096  bclbnd  27172  bposlem8  27183  lgsdir2lem1  27217  lgsdir2lem5  27221  lgseisenlem1  27267  lgseisenlem2  27268  lgsquadlem1  27272  chebbnd1  27364  dchrvmasumlem2  27390  norecfn  27843  norec2fn  27853  addsproplem2  27867  addsproplem6  27871  addsbdaylem  27913  negs1s  27923  negsproplem2  27925  mulsproplem2  28010  mulsproplem3  28011  mulsproplem5  28013  mulsproplem6  28014  mulsproplem7  28015  mulsproplem8  28016  mulsproplem13  28021  mulsproplem14  28022  0zs  28266  zseo  28299  twocut  28300  istrkg3ld  28393  trgcgrg  28447  ax5seglem7  28867  axlowdimlem6  28879  axlowdimlem8  28881  axlowdimlem11  28884  elntg2  28917  cusgrsizeindb1  29383  vtxdginducedm1  29476  0grrusgr  29512  erclwwlktr  29953  erclwwlkntr  30002  wlk2v2e  30088  upgr3v3e3cycl  30111  konigsberglem1  30183  konigsberglem2  30184  konigsberglem3  30185  konigsberglem5  30187  ex-fl  30378  ex-mod  30380  ex-hash  30384  ex-lcm  30389  0vfval  30537  smcnlem  30628  lnocoi  30688  nmlno0lem  30724  nmblolbii  30730  blocnilem  30735  blocni  30736  cncph  30750  isph  30753  ip0i  30756  ip1ilem  30757  ip2i  30759  ipdirilem  30760  ipasslem7  30767  ipasslem8  30768  ipasslem9  30769  ipasslem10  30770  ipasslem11  30771  ip2dii  30775  pythi  30781  siilem1  30782  siilem2  30783  siii  30784  hvmulassi  30977  hvmulcomi  30978  hvdistr1i  30982  hvsubdistr1i  30983  hvassi  30984  hvadd32i  30985  hvsubassi  30986  hvsub32i  30987  normlem0  31040  normlem8  31048  normlem9  31049  bcseqi  31051  polid2i  31088  hhph  31109  hlim0  31166  shscli  31248  shlessi  31308  shlej1i  31309  omlsilem  31333  shlubi  31346  h1de2i  31484  pjadjii  31605  pjaddii  31606  pjmulii  31608  pjdifnormii  31614  pjcji  31615  hoaddsubassi  31751  eigrei  31765  eigposi  31767  eigorthi  31768  adj0  31925  lnopeq0lem1  31936  lnopunilem1  31941  lnophmlem2  31948  nmcexi  31957  nmcopexi  31958  lnfn0i  31973  nmcfnexi  31982  mdexchi  32266  xppreima2  32585  sgnclre  32770  dp2clq  32816  dp2lt  32820  dp2ltc  32822  dpexpp1  32843  dpmul  32848  dpmul4  32849  elxrge02  32867  xrge0adddir  32967  psgnid  33034  cnmsgn0g  33083  altgnsg  33086  xrnarchi  33121  xrge0slmod  33281  znfermltl  33299  ccfldextdgrr  33653  cos9thpiminplylem4  33766  cos9thpiminplylem5  33767  raddcn  33910  xrge0iifcnv  33914  xrge0iifiso  33916  xrge0iifhmeo  33917  xrge0iifhom  33918  xrge0iifmhm  33920  xrge0mulc1cn  33922  lmlimxrge0  33929  pnfneige0  33932  lmxrge0  33933  zringnm  33939  rezh  33950  qqh0  33965  qqh1  33966  qqhucn  33973  esumpinfval  34054  hashf2  34065  esumcvg  34067  br2base  34250  sxbrsigalem3  34253  dya2iocbrsiga  34256  dya2icobrsiga  34257  sxbrsigalem1  34266  sxbrsigalem2  34267  sxbrsigalem4  34268  sxbrsigalem5  34269  sxbrsiga  34271  ballotlem2  34470  ballotlem4  34480  ballotlemi1  34484  ballotth  34519  signstf  34547  itgexpif  34587  chtvalz  34610  hgt750lemd  34629  hgt750lem  34632  tgoldbachgnn  34640  lfuhgr2  35109  subfacp1lem1  35169  subfacp1lem6  35175  kur14lem6  35201  cvmliftlem4  35278  satf0suc  35366  problem4  35658  quad3  35660  iexpire  35725  fununiq  35759  fvtransport  36023  bj-minftyccb  37216  taupilem2  37313  iccioo01  37318  1oequni2o  37359  finxp1o  37383  finxpreclem4  37385  cos2h  37608  tan2h  37609  poimirlem9  37626  poimirlem27  37644  poimirlem28  37645  ismblfin  37658  mbfposadd  37664  ftc1anclem5  37694  asindmre  37700  dvasin  37701  dvacos  37702  rrnval  37824  dihjatcclem4  41417  lcmineqlem12  42030  fisdomnn  42234  subex  42237  absex  42238  cjex  42239  cxpi11d  42333  redvmptabs  42350  readvrec  42352  sn-00idlem2  42389  sn-00id  42391  remul02  42395  rabren3dioph  42805  jm2.27dlem2  43000  rmydioph  43004  rmxdioph  43006  expdiophlem2  43012  expdioph  43013  arearect  43205  areaquad  43206  2omomeqom  43293  omnord1ex  43294  corclrcl  43697  iunrelexpuztr  43709  corcltrcl  43729  dffrege76  43929  k0004val0  44144  lhe4.4ex1a  44319  binomcxplemdvbinom  44343  binomcxplemnotnn0  44346  ax6e2ndeqALT  44920  sineq0ALT  44926  nregmodelf1o  45005  pnfel0pnf  45525  lptioo2cn  45640  limsup10ex  45768  liminf10ex  45769  icccncfext  45882  itgsin0pilem1  45945  itgsbtaddcnst  45977  stoweidlem13  46008  wallispilem2  46061  wallispilem4  46063  wallispi2lem1  46066  stirlinglem13  46081  dirkerper  46091  dirkertrigeqlem3  46095  dirkeritg  46097  dirkercncflem1  46098  dirkercncflem4  46101  fourierdlem42  46144  fourierdlem62  46163  fourierdlem102  46203  fourierdlem103  46204  fourierdlem104  46205  fourierdlem114  46215  sqwvfoura  46223  fourierswlem  46225  fouriersw  46226  smfmullem4  46789  ceil5half3  47338  8mod5e3  47358  fmtnoprmfac2lem1  47564  fmtno4prm  47573  3exp4mod41  47614  41prothprmlem2  47616  6gbe  47769  7gbow  47770  8gbe  47771  9gbo  47772  11gbo  47773  sbgoldbalt  47779  nnsum4primesevenALTV  47799  usgrexmpl2nb0  48029  usgrexmpl2nb3  48032  gpg3nbgrvtx0  48074  gpg3nbgrvtx0ALT  48075  gpg3nbgrvtx1  48076  gpg5grlim  48091  gpg5grlic  48092  0nodd  48168  oddinmgm  48173  2zrng0  48242  zlmodzxz0  48354  zlmodzxzequa  48495  zlmodzxzequap  48498  zlmodzxzldeplem3  48501  nnlog2ge0lt1  48565  blen1  48583  blen2  48584  nnolog2flm1  48589  ackval42  48695  ehl2eudisval0  48724  line2ylem  48750  i0oii  48918  io1ii  48919  sepfsepc  48926  rescofuf  49092  setc1ohomfval  49492  setc1ocofval  49493