Theorem mp3an 1484

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

Syntax hints:   → wi 4   ∧ w3a 1099

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 400  df-3an 1101

This theorem is referenced by:  el3v  3464  raltp  4666  rextp  4667  opthhausdorff  5488  funopg  6557  feq12i  6686  ftp  7142  caovass  7598  caovdi  7617  ordom  7858  mptexw  7936  ofmres  7967  sbcoteq1a  8034  mpoexw  8061  xpord3lem  8131  omopthlem1  8631  omopthlem2  8632  omopthi  8633  on2recsfn  8639  xpcomen  9042  snnen2o  9191  unfilem3  9253  hartogs  9494  card2on  9504  unwf  9770  inlresf1  9875  inrresf1  9877  tskwe  9910  alephsmo  10060  dfac4  10080  dfac2a  10088  ackbij1lem13  10189  axdc2lem  10407  axcclem  10416  ondomon  10522  cfpwsdom  10544  pwfseqlem2  10619  pwfseqlem3  10620  1lt2pi  10865  addassi  11194  mulassi  11195  adddii  11196  adddiri  11197  lttri  11311  lelttri  11312  ltletri  11313  letri  11314  ltadd2i  11316  mul02lem2  11362  addrid  11365  addcani  11378  addcan2i  11379  mul12i  11380  mul32i  11381  add12i  11408  add32i  11409  subaddi  11520  subadd2i  11521  subsub23i  11523  addsubassi  11524  addsubi  11525  subcani  11526  subcan2i  11527  pnncani  11528  subdii  11638  subdiri  11639  ltadd1i  11743  leadd1i  11744  leadd2i  11745  ltsubaddi  11746  lesubaddi  11747  ltsubadd2i  11748  lesubadd2i  11749  ltaddsubi  11750  mulcani  11828  div23i  11951  div11i  11952  3halfnz  12654  mpoaddex  12991  addex  12992  mpomulex  12993  mulex  12994  unirnioo  13455  ioorebas  13457  xnn0xrge0  13512  fldiv4lem1div2  13849  uzenom  13979  nnenom  13995  seqexw  14032  m1expcl2  14100  i4  14219  expnass  14223  faclbnd4lem1  14308  bcn1  14328  hashfxnn0  14352  ccat2s1p1  14645  ccat2s1p2  14646  cats1fvn  14873  cats1fv  14874  cats1cat  14876  cats2cat  14877  wrdlen3s3  14964  sgnrn  15113  sgnclre  15117  abs3difi  15439  0.999...  15913  bpoly3  16090  ef01bndlem  16218  cos1bnd  16221  cos2bnd  16222  sin4lt0  16229  rpnnen2lem3  16250  rpnnen2lem11  16258  rpnnen  16261  rexpen  16262  aleph1irr  16280  3dvdsdec  16368  3dvds2dec  16369  divalglem2  16431  ndvdsi  16448  flodddiv4  16451  gcdaddmlem  16560  bezout  16579  3lcm2e6woprm  16651  6lcm4e12  16652  lcmf0  16670  lcmf2a3a4e12  16683  dec2dvds  17101  modxai  17106  modsubi  17110  gcdi  17111  numexp2x  17116  2exp5  17123  2exp11  17127  ex-chn2  18672  0symgefmndeq  19436  pmtrprfval  19529  m1expaddsub  19540  0frgp  19821  staffval  20892  cnfldcj  21435  cnfldds  21438  cnfldfunALT  21441  xrsadd  21444  xrsmul  21445  xrsds  21464  cnmgpid  21483  nn0srg  21491  rge0srg  21492  zring0  21512  pzriprnglem13  21547  pzriprng1ALT  21550  fermltlchr  21583  cnmsgnsubg  21631  psgninv  21636  re0g  21666  ocvfval  21720  frlmbas  21809  mdetrlin  22664  mdetunilem9  22682  leordtval2  23274  iscnp2  23301  utop3cls  24313  nmfval  24650  nmoffn  24773  nmofval  24776  icccld  24828  addcnlem  24927  iimulcn  25002  icopnfhmeo  25007  iccpnfcnv  25008  iccpnfhmeo  25009  xrhmeo  25010  xrhmph  25011  oprpiece1res1  25015  oprpiece1res2  25016  ishtpy  25036  pcoass  25088  cnstrcvs  25205  cncvs  25209  recvs  25210  qcvs  25211  zclmncvs  25212  tcphex  25281  cnfldcusp  25421  resscdrg  25422  reust  25445  recusp  25446  vitalilem4  25675  vitalilem5  25676  mbfdm  25690  dveflem  26043  dvlipcn  26058  c1lip2  26062  dgrid  26326  iaa  26391  abelthlem3  26498  abelthlem5  26500  abelth  26506  efcn  26508  sinhalfpilem  26530  sincosq1lem  26564  sincosq4sgn  26568  tangtx  26572  sincos4thpi  26580  sincos6thpi  26583  pigt3  26585  pige3ALT  26587  cos0pilt1  26599  logi  26654  relogcn  26705  dvlog2lem  26719  dvlog2  26720  logtayl  26727  logtayl2  26729  cxpsqrtlem  26769  cxpsqrt  26770  2irrexpq  26798  cxpcn2  26813  cxpcn3  26815  logblog  26859  2logb9irr  26862  2logb3irr  26864  2logb9irrALT  26865  sqrt2cxp2logb9e3  26866  2irrexpqALT  26867  ang180lem1  26876  ang180lem2  26877  1cubrlem  26908  mcubic  26914  quart1lem  26922  quart1  26923  reasinsin  26963  atancj  26977  efiatan  26979  atantan  26990  atanbndlem  26992  atan1  26995  atancn  27003  atantayl2  27005  log2cnv  27011  log2tlbnd  27012  log2ublem1  27013  log2ublem2  27014  log2ub  27016  efrlim  27036  scvxcvx  27052  1sgm2ppw  27266  ppiub  27270  bclbnd  27346  bposlem8  27357  lgsdir2lem1  27391  lgsdir2lem5  27395  lgseisenlem1  27441  lgseisenlem2  27442  lgsquadlem1  27446  chebbnd1  27538  dchrvmasumlem2  27564  norecfn  28041  norec2fn  28051  addsproplem2  28065  addsproplem6  28069  addbdaylem  28112  neg1s  28122  negsproplem2  28124  mulsproplem2  28212  mulsproplem3  28213  mulsproplem5  28215  mulsproplem6  28216  mulsproplem7  28217  mulsproplem8  28218  mulsproplem13  28223  mulsproplem14  28224  0zs  28483  zseo  28517  twocut  28518  bdaypw2n0bndlem  28558  bdaypw2bnd  28560  bdayfinbndlem1  28562  z12bdaylem2  28566  istrkg3ld  28632  trgcgrg  28686  ax5seglem7  29138  axlowdimlem6  29150  axlowdimlem8  29152  axlowdimlem11  29155  elntg2  29188  cusgrsizeindb1  29653  vtxdginducedm1  29746  0grrusgr  29782  erclwwlktr  30226  erclwwlkntr  30275  wlk2v2e  30361  upgr3v3e3cycl  30384  konigsberglem1  30456  konigsberglem2  30457  konigsberglem3  30458  konigsberglem5  30460  ex-fl  30651  ex-mod  30653  ex-hash  30657  ex-lcm  30662  0vfval  30811  smcnlem  30902  lnocoi  30962  nmlno0lem  30998  nmblolbii  31004  blocnilem  31009  blocni  31010  cncph  31024  isph  31027  ip0i  31030  ip1ilem  31031  ip2i  31033  ipdirilem  31034  ipasslem7  31041  ipasslem8  31042  ipasslem9  31043  ipasslem10  31044  ipasslem11  31045  ip2dii  31049  pythi  31055  siilem1  31056  siilem2  31057  siii  31058  hvmulassi  31251  hvmulcomi  31252  hvdistr1i  31256  hvsubdistr1i  31257  hvassi  31258  hvadd32i  31259  hvsubassi  31260  hvsub32i  31261  normlem0  31314  normlem8  31322  normlem9  31323  bcseqi  31325  polid2i  31362  hhph  31383  hlim0  31440  shscli  31522  shlessi  31582  shlej1i  31583  omlsilem  31607  shlubi  31620  h1de2i  31758  pjadjii  31879  pjaddii  31880  pjmulii  31882  pjdifnormii  31888  pjcji  31889  hoaddsubassi  32025  eigrei  32039  eigposi  32041  eigorthi  32042  adj0  32199  lnopeq0lem1  32210  lnopunilem1  32215  lnophmlem2  32222  nmcexi  32231  nmcopexi  32232  lnfn0i  32247  nmcfnexi  32256  mdexchi  32540  xppreima2  32855  dp2clq  33060  dp2lt  33064  dp2ltc  33066  dpexpp1  33087  dpmul  33092  dpmul4  33093  elxrge02  33111  xrge0adddir  33198  psgnid  33279  cnmsgn0g  33328  altgnsg  33331  xrnarchi  33366  xrge0slmod  33536  znfermltl  33554  ccfldextdgrr  33971  cos9thpiminplylem4  34084  cos9thpiminplylem5  34085  raddcn  34228  xrge0iifcnv  34232  xrge0iifiso  34234  xrge0iifhmeo  34235  xrge0iifhom  34236  xrge0iifmhm  34238  xrge0mulc1cn  34240  lmlimxrge0  34247  pnfneige0  34250  lmxrge0  34251  zringnm  34257  rezh  34268  qqh0  34283  qqh1  34284  qqhucn  34291  esumpinfval  34372  hashf2  34383  esumcvg  34385  br2base  34568  sxbrsigalem3  34571  dya2iocbrsiga  34574  dya2icobrsiga  34575  sxbrsigalem1  34584  sxbrsigalem2  34585  sxbrsigalem4  34586  sxbrsigalem5  34587  sxbrsiga  34589  ballotlem2  34788  ballotlem4  34798  ballotlemi1  34802  ballotth  34837  signstf  34862  itgexpif  34902  chtvalz  34925  hgt750lemd  34944  hgt750lem  34947  tgoldbachgnn  34955  lfuhgr2  35474  subfacp1lem1  35534  subfacp1lem6  35540  kur14lem6  35566  cvmliftlem4  35643  satf0suc  35731  problem4  36023  quad3  36025  iexpire  36090  fununiq  36124  fvtransport  36387  ttcid  36857  dfttc2g  36871  bj-minftyccb  37722  taupilem2  37819  iccioo01  37826  1oequni2o  37867  finxp1o  37891  finxpreclem4  37893  cos2h  38115  tan2h  38116  poimirlem9  38133  poimirlem27  38151  poimirlem28  38152  ismblfin  38165  mbfposadd  38171  ftc1anclem5  38201  asindmre  38207  dvasin  38208  dvacos  38209  rrnval  38331  dihjatcclem4  42050  lcmineqlem12  42662  fisdomnn  42865  subex  42868  absex  42869  cjex  42870  cxpi11d  42957  redvmptabs  42974  readvrec  42976  sn-00idlem2  43013  sn-00id  43015  remul02  43019  rabren3dioph  43397  jm2.27dlem2  43592  rmydioph  43596  rmxdioph  43598  expdiophlem2  43604  expdioph  43605  arearect  43797  areaquad  43798  2omomeqom  43885  omnord1ex  43886  corclrcl  44288  iunrelexpuztr  44300  corcltrcl  44320  dffrege76  44520  k0004val0  44735  lhe4.4ex1a  44910  binomcxplemdvbinom  44934  binomcxplemnotnn0  44937  ax6e2ndeqALT  45511  sineq0ALT  45517  nregmodelf1o  45596  pnfel0pnf  46109  lptioo2cn  46224  limsup10ex  46352  liminf10ex  46353  icccncfext  46466  itgsin0pilem1  46529  itgsbtaddcnst  46561  stoweidlem13  46592  wallispilem2  46645  wallispilem4  46647  wallispi2lem1  46650  stirlinglem13  46665  dirkerper  46675  dirkertrigeqlem3  46679  dirkeritg  46681  dirkercncflem1  46682  dirkercncflem4  46685  fourierdlem42  46728  fourierdlem62  46747  fourierdlem102  46787  fourierdlem103  46788  fourierdlem104  46789  fourierdlem114  46799  sqwvfoura  46807  fourierswlem  46809  fouriersw  46810  smfmullem4  47373  nthrucw  47467  goldracos5teq  47484  goldratmolem2  47485  ceil5half3  47945  8mod5e3  47965  fmtnoprmfac2lem1  48180  fmtno4prm  48189  3exp4mod41  48230  41prothprmlem2  48232  ppivalnn4  48241  6gbe  48398  7gbow  48399  8gbe  48400  9gbo  48401  11gbo  48402  sbgoldbalt  48408  nnsum4primesevenALTV  48428  usgrexmpl2nb0  48658  usgrexmpl2nb3  48661  gpg3nbgrvtx0  48703  gpg3nbgrvtx0ALT  48704  gpg3nbgrvtx1  48705  gpg5grlim  48720  gpg5grlic  48721  0nodd  48797  oddinmgm  48802  2zrng0  48871  zlmodzxz0  48983  zlmodzxzequa  49123  zlmodzxzequap  49126  zlmodzxzldeplem3  49129  nnlog2ge0lt1  49193  blen1  49211  blen2  49212  nnolog2flm1  49217  ackval42  49323  ehl2eudisval0  49352  line2ylem  49378  i0oii  49546  io1ii  49547  sepfsepc  49554  rescofuf  49719  setc1ohomfval  50119  setc1ocofval  50120