Theorem mp3an 1460

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 1447	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 689	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  raltp  4647  rextp  4648  opthhausdorff  5435  funopg  6466  feq12i  6591  ftp  7026  caovass  7466  caovdi  7485  ordom  7716  mptexw  7789  ofmres  7820  mpoexw  7912  omopthlem1  8472  omopthlem2  8473  omopthi  8474  xpcomen  8832  unfilem3  9058  hartogs  9281  card2on  9291  unwf  9569  inlresf1  9674  inrresf1  9676  tskwe  9709  alephsmo  9859  dfac4  9879  dfac2a  9886  ackbij1lem13  9989  axdc2lem  10205  axcclem  10214  ondomon  10320  cfpwsdom  10341  pwfseqlem2  10416  pwfseqlem3  10417  1lt2pi  10662  addassi  10986  mulassi  10987  adddii  10988  adddiri  10989  lttri  11101  lelttri  11102  ltletri  11103  letri  11104  ltadd2i  11106  mul02lem2  11152  addid1  11155  addcani  11168  addcan2i  11169  mul12i  11170  mul32i  11171  add12i  11197  add32i  11198  subaddi  11308  subadd2i  11309  subsub23i  11311  addsubassi  11312  addsubi  11313  subcani  11314  subcan2i  11315  pnncani  11316  subdii  11424  subdiri  11425  ltadd1i  11529  leadd1i  11530  leadd2i  11531  ltsubaddi  11532  lesubaddi  11533  ltsubadd2i  11534  lesubadd2i  11535  ltaddsubi  11536  mulcani  11614  div23i  11733  div11i  11734  1mhlfehlf  12192  halfpm6th  12194  3halfnz  12399  addex  12727  mulex  12728  unirnioo  13180  ioorebas  13182  xnn0xrge0  13237  fldiv4lem1div2  13555  uzenom  13682  nnenom  13698  seqexw  13735  m1expcl2  13802  i4  13919  expnass  13922  faclbnd4lem1  14005  bcn1  14025  hashfxnn0  14049  ccat2s1p1  14334  ccat2s1p2  14335  cats1fvn  14569  cats1fv  14570  cats1cat  14572  cats2cat  14573  wrdlen3s3  14660  abs3difi  15119  0.999...  15591  bpoly3  15766  ef01bndlem  15891  cos1bnd  15894  cos2bnd  15895  sin4lt0  15902  rpnnen2lem3  15923  rpnnen2lem11  15931  rpnnen  15934  rexpen  15935  aleph1irr  15953  3dvdsdec  16039  3dvds2dec  16040  divalglem2  16102  ndvdsi  16119  flodddiv4  16120  gcdaddmlem  16229  bezout  16249  3lcm2e6woprm  16318  6lcm4e12  16319  lcmf0  16337  lcmf2a3a4e12  16350  dec2dvds  16762  modxai  16767  modsubi  16771  gcdi  16772  numexp2x  16778  2exp5  16785  2exp11  16789  0symgefmndeq  18999  pmtrprfval  19093  m1expaddsub  19104  0frgp  19383  staffval  20105  cnfldcj  20602  cnfldds  20605  cnfldfun  20607  cnfldfunOLD  20608  xrsadd  20613  xrsmul  20614  xrsds  20639  cnmgpid  20658  nn0srg  20666  rge0srg  20667  zring0  20678  cnmsgnsubg  20780  psgninv  20785  re0g  20815  ocvfval  20869  frlmbas  20960  mdetrlin  21749  mdetunilem9  21767  leordtval2  22361  iscnp2  22388  utop3cls  23401  nmfval  23742  nmoffn  23873  nmofval  23876  icccld  23928  addcnlem  24025  iimulcn  24099  icopnfhmeo  24104  iccpnfcnv  24105  iccpnfhmeo  24106  xrhmeo  24107  xrhmph  24108  oprpiece1res1  24112  oprpiece1res2  24113  ishtpy  24133  pcoass  24185  cnstrcvs  24302  cncvs  24306  recvs  24307  recvsOLD  24308  qcvs  24309  zclmncvs  24310  tcphex  24379  cnfldcusp  24519  resscdrg  24520  reust  24543  recusp  24544  vitalilem4  24773  vitalilem5  24774  mbfdm  24788  dveflem  25141  dvlipcn  25156  c1lip2  25160  dgrid  25423  iaa  25483  abelthlem3  25590  abelthlem5  25592  abelth  25598  efcn  25600  sinhalfpilem  25618  sincosq1lem  25652  sincosq4sgn  25656  tangtx  25660  sincos4thpi  25668  sincos6thpi  25670  pigt3  25672  pige3ALT  25674  cos0pilt1  25686  relogcn  25791  dvlog2lem  25805  dvlog2  25806  logtayl  25813  logtayl2  25815  cxpsqrtlem  25855  cxpsqrt  25856  2irrexpq  25883  cxpcn2  25897  cxpcn3  25899  logblog  25940  2logb9irr  25943  2logb3irr  25945  2logb9irrALT  25946  sqrt2cxp2logb9e3  25947  2irrexpqALT  25948  ang180lem1  25957  ang180lem2  25958  1cubrlem  25989  mcubic  25995  quart1lem  26003  quart1  26004  reasinsin  26044  atancj  26058  efiatan  26060  atantan  26071  atanbndlem  26073  atan1  26076  atancn  26084  atantayl2  26086  log2cnv  26092  log2tlbnd  26093  log2ublem1  26094  log2ublem2  26095  log2ub  26097  efrlim  26117  scvxcvx  26133  1sgm2ppw  26346  ppiub  26350  bclbnd  26426  bposlem8  26437  lgsdir2lem1  26471  lgsdir2lem5  26475  lgseisenlem1  26521  lgseisenlem2  26522  lgsquadlem1  26526  chebbnd1  26618  dchrvmasumlem2  26644  istrkg3ld  26820  trgcgrg  26874  ax5seglem7  27301  axlowdimlem6  27313  axlowdimlem8  27315  axlowdimlem11  27318  elntg2  27351  cusgrsizeindb1  27815  vtxdginducedm1  27908  0grrusgr  27944  erclwwlktr  28382  erclwwlkntr  28431  wlk2v2e  28517  upgr3v3e3cycl  28540  konigsberglem1  28612  konigsberglem2  28613  konigsberglem3  28614  konigsberglem5  28616  ex-fl  28807  ex-mod  28809  ex-hash  28813  ex-lcm  28818  0vfval  28964  smcnlem  29055  lnocoi  29115  nmlno0lem  29151  nmblolbii  29157  blocnilem  29162  blocni  29163  cncph  29177  isph  29180  ip0i  29183  ip1ilem  29184  ip2i  29186  ipdirilem  29187  ipasslem7  29194  ipasslem8  29195  ipasslem9  29196  ipasslem10  29197  ipasslem11  29198  ip2dii  29202  pythi  29208  siilem1  29209  siilem2  29210  siii  29211  hvmulassi  29404  hvmulcomi  29405  hvdistr1i  29409  hvsubdistr1i  29410  hvassi  29411  hvadd32i  29412  hvsubassi  29413  hvsub32i  29414  normlem0  29467  normlem8  29475  normlem9  29476  bcseqi  29478  polid2i  29515  hhph  29536  hlim0  29593  shscli  29675  shlessi  29735  shlej1i  29736  omlsilem  29760  shlubi  29773  h1de2i  29911  pjadjii  30032  pjaddii  30033  pjmulii  30035  pjdifnormii  30041  pjcji  30042  hoaddsubassi  30178  eigrei  30192  eigposi  30194  eigorthi  30195  adj0  30352  lnopeq0lem1  30363  lnopunilem1  30368  lnophmlem2  30375  nmcexi  30384  nmcopexi  30385  lnfn0i  30400  nmcfnexi  30409  mdexchi  30693  xppreima2  30984  dp2clq  31151  dp2lt  31155  dp2ltc  31157  dpexpp1  31178  dpmul  31183  dpmul4  31184  elxrge02  31202  xrge0adddir  31297  psgnid  31360  cnmsgn0g  31409  altgnsg  31412  xrnarchi  31434  xrge0slmod  31544  znfermltl  31558  ccfldextdgrr  31738  raddcn  31875  xrge0iifcnv  31879  xrge0iifiso  31881  xrge0iifhmeo  31882  xrge0iifhom  31883  xrge0iifmhm  31885  xrge0mulc1cn  31887  lmlimxrge0  31894  pnfneige0  31897  lmxrge0  31898  zringnm  31904  rezh  31917  qqh0  31930  qqh1  31931  qqhucn  31938  esumpinfval  32037  hashf2  32048  esumcvg  32050  br2base  32232  sxbrsigalem3  32235  dya2iocbrsiga  32238  dya2icobrsiga  32239  sxbrsigalem1  32248  sxbrsigalem2  32249  sxbrsigalem4  32250  sxbrsigalem5  32251  sxbrsiga  32253  ballotlem2  32451  ballotlem4  32461  ballotlemi1  32465  ballotth  32500  sgnclre  32502  signstf  32541  itgexpif  32582  chtvalz  32605  hgt750lemd  32624  hgt750lem  32627  tgoldbachgnn  32635  lfuhgr2  33076  subfacp1lem1  33137  subfacp1lem6  33143  kur14lem6  33169  cvmliftlem4  33246  satf0suc  33334  problem4  33622  quad3  33624  logi  33696  iexpire  33697  fununiq  33739  on2recsfn  33822  norecfn  34099  norec2fn  34109  fvtransport  34330  bj-minftyccb  35392  taupilem2  35489  iccioo01  35494  1oequni2o  35535  finxp1o  35559  finxpreclem4  35561  cos2h  35764  tan2h  35765  poimirlem9  35782  poimirlem27  35800  poimirlem28  35801  ismblfin  35814  mbfposadd  35820  ftc1anclem5  35850  asindmre  35856  dvasin  35857  dvacos  35858  rrnval  35981  el3v  36367  dihjatcclem4  39431  lcmineqlem12  40045  sn-00idlem2  40379  sn-00id  40381  remul02  40385  rei4  40402  sn-0lt1  40429  rabren3dioph  40634  jm2.27dlem2  40829  rmydioph  40833  rmxdioph  40835  expdiophlem2  40841  expdioph  40842  arearect  41043  areaquad  41044  corclrcl  41285  iunrelexpuztr  41297  corcltrcl  41317  dffrege76  41517  k0004val0  41734  lhe4.4ex1a  41917  binomcxplemdvbinom  41941  binomcxplemnotnn0  41944  ax6e2ndeqALT  42521  sineq0ALT  42527  pnfel0pnf  43037  lptioo2cn  43157  limsup10ex  43285  liminf10ex  43286  icccncfext  43399  itgsin0pilem1  43462  itgsbtaddcnst  43494  stoweidlem13  43525  wallispilem2  43578  wallispilem4  43580  wallispi2lem1  43583  stirlinglem13  43598  dirkerper  43608  dirkertrigeqlem3  43612  dirkeritg  43614  dirkercncflem1  43615  dirkercncflem4  43618  fourierdlem42  43661  fourierdlem62  43680  fourierdlem102  43720  fourierdlem103  43721  fourierdlem104  43722  fourierdlem114  43732  sqwvfoura  43740  fourierswlem  43742  fouriersw  43743  smfmullem4  44296  fmtnoprmfac2lem1  44987  fmtno4prm  44996  3exp4mod41  45037  41prothprmlem2  45039  6gbe  45192  7gbow  45193  8gbe  45194  9gbo  45195  11gbo  45196  sbgoldbalt  45202  nnsum4primesevenALTV  45222  0nodd  45333  oddinmgm  45338  2zrng0  45465  zlmodzxz0  45661  zlmodzxzequa  45806  zlmodzxzequap  45809  zlmodzxzldeplem3  45812  nnlog2ge0lt1  45881  blen1  45899  blen2  45900  nnolog2flm1  45905  ackval42  46011  ehl2eudisval0  46040  line2ylem  46066  i0oii  46182  io1ii  46183  sepfsepc  46190