Theorem mp3an 1462

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  raltp  4710  rextp  4711  opthhausdorff  5518  funopg  6583  feq12i  6711  ftp  7155  caovass  7607  caovdi  7626  ordom  7865  mptexw  7939  ofmres  7971  sbcoteq1a  8037  mpoexw  8065  xpord3lem  8135  omopthlem1  8658  omopthlem2  8659  omopthi  8660  on2recsfn  8666  xpcomen  9063  snnen2o  9237  unfilem3  9312  hartogs  9539  card2on  9549  unwf  9805  inlresf1  9910  inrresf1  9912  tskwe  9945  alephsmo  10097  dfac4  10117  dfac2a  10124  ackbij1lem13  10227  axdc2lem  10443  axcclem  10452  ondomon  10558  cfpwsdom  10579  pwfseqlem2  10654  pwfseqlem3  10655  1lt2pi  10900  addassi  11224  mulassi  11225  adddii  11226  adddiri  11227  lttri  11340  lelttri  11341  ltletri  11342  letri  11343  ltadd2i  11345  mul02lem2  11391  addrid  11394  addcani  11407  addcan2i  11408  mul12i  11409  mul32i  11410  add12i  11436  add32i  11437  subaddi  11547  subadd2i  11548  subsub23i  11550  addsubassi  11551  addsubi  11552  subcani  11553  subcan2i  11554  pnncani  11555  subdii  11663  subdiri  11664  ltadd1i  11768  leadd1i  11769  leadd2i  11770  ltsubaddi  11771  lesubaddi  11772  ltsubadd2i  11773  lesubadd2i  11774  ltaddsubi  11775  mulcani  11853  div23i  11972  div11i  11973  1mhlfehlf  12431  halfpm6th  12433  3halfnz  12641  addex  12972  mulex  12973  unirnioo  13426  ioorebas  13428  xnn0xrge0  13483  fldiv4lem1div2  13802  uzenom  13929  nnenom  13945  seqexw  13982  m1expcl2  14051  i4  14168  expnass  14172  faclbnd4lem1  14253  bcn1  14273  hashfxnn0  14297  ccat2s1p1  14579  ccat2s1p2  14580  cats1fvn  14809  cats1fv  14810  cats1cat  14812  cats2cat  14813  wrdlen3s3  14900  abs3difi  15356  0.999...  15827  bpoly3  16002  ef01bndlem  16127  cos1bnd  16130  cos2bnd  16131  sin4lt0  16138  rpnnen2lem3  16159  rpnnen2lem11  16167  rpnnen  16170  rexpen  16171  aleph1irr  16189  3dvdsdec  16275  3dvds2dec  16276  divalglem2  16338  ndvdsi  16355  flodddiv4  16356  gcdaddmlem  16465  bezout  16485  3lcm2e6woprm  16552  6lcm4e12  16553  lcmf0  16571  lcmf2a3a4e12  16584  dec2dvds  16996  modxai  17001  modsubi  17005  gcdi  17006  numexp2x  17012  2exp5  17019  2exp11  17023  0symgefmndeq  19261  pmtrprfval  19355  m1expaddsub  19366  0frgp  19647  staffval  20455  cnfldcj  20951  cnfldds  20954  cnfldfunALT  20957  cnfldfunALTOLD  20958  xrsadd  20962  xrsmul  20963  xrsds  20988  cnmgpid  21007  nn0srg  21015  rge0srg  21016  zring0  21028  cnmsgnsubg  21130  psgninv  21135  re0g  21165  ocvfval  21219  frlmbas  21310  mdetrlin  22104  mdetunilem9  22122  leordtval2  22716  iscnp2  22743  utop3cls  23756  nmfval  24097  nmoffn  24228  nmofval  24231  icccld  24283  addcnlem  24380  iimulcn  24454  icopnfhmeo  24459  iccpnfcnv  24460  iccpnfhmeo  24461  xrhmeo  24462  xrhmph  24463  oprpiece1res1  24467  oprpiece1res2  24468  ishtpy  24488  pcoass  24540  cnstrcvs  24657  cncvs  24661  recvs  24662  recvsOLD  24663  qcvs  24664  zclmncvs  24665  tcphex  24734  cnfldcusp  24874  resscdrg  24875  reust  24898  recusp  24899  vitalilem4  25128  vitalilem5  25129  mbfdm  25143  dveflem  25496  dvlipcn  25511  c1lip2  25515  dgrid  25778  iaa  25838  abelthlem3  25945  abelthlem5  25947  abelth  25953  efcn  25955  sinhalfpilem  25973  sincosq1lem  26007  sincosq4sgn  26011  tangtx  26015  sincos4thpi  26023  sincos6thpi  26025  pigt3  26027  pige3ALT  26029  cos0pilt1  26041  relogcn  26146  dvlog2lem  26160  dvlog2  26161  logtayl  26168  logtayl2  26170  cxpsqrtlem  26210  cxpsqrt  26211  2irrexpq  26239  cxpcn2  26254  cxpcn3  26256  logblog  26297  2logb9irr  26300  2logb3irr  26302  2logb9irrALT  26303  sqrt2cxp2logb9e3  26304  2irrexpqALT  26305  ang180lem1  26314  ang180lem2  26315  1cubrlem  26346  mcubic  26352  quart1lem  26360  quart1  26361  reasinsin  26401  atancj  26415  efiatan  26417  atantan  26428  atanbndlem  26430  atan1  26433  atancn  26441  atantayl2  26443  log2cnv  26449  log2tlbnd  26450  log2ublem1  26451  log2ublem2  26452  log2ub  26454  efrlim  26474  scvxcvx  26490  1sgm2ppw  26703  ppiub  26707  bclbnd  26783  bposlem8  26794  lgsdir2lem1  26828  lgsdir2lem5  26832  lgseisenlem1  26878  lgseisenlem2  26879  lgsquadlem1  26883  chebbnd1  26975  dchrvmasumlem2  27001  norecfn  27430  norec2fn  27440  addsproplem2  27454  addsproplem6  27458  negsproplem2  27503  mulsproplem2  27573  mulsproplem3  27574  mulsproplem5  27576  mulsproplem6  27577  mulsproplem7  27578  mulsproplem8  27579  mulsproplem13  27584  mulsproplem14  27585  istrkg3ld  27712  trgcgrg  27766  ax5seglem7  28193  axlowdimlem6  28205  axlowdimlem8  28207  axlowdimlem11  28210  elntg2  28243  cusgrsizeindb1  28707  vtxdginducedm1  28800  0grrusgr  28836  erclwwlktr  29275  erclwwlkntr  29324  wlk2v2e  29410  upgr3v3e3cycl  29433  konigsberglem1  29505  konigsberglem2  29506  konigsberglem3  29507  konigsberglem5  29509  ex-fl  29700  ex-mod  29702  ex-hash  29706  ex-lcm  29711  0vfval  29859  smcnlem  29950  lnocoi  30010  nmlno0lem  30046  nmblolbii  30052  blocnilem  30057  blocni  30058  cncph  30072  isph  30075  ip0i  30078  ip1ilem  30079  ip2i  30081  ipdirilem  30082  ipasslem7  30089  ipasslem8  30090  ipasslem9  30091  ipasslem10  30092  ipasslem11  30093  ip2dii  30097  pythi  30103  siilem1  30104  siilem2  30105  siii  30106  hvmulassi  30299  hvmulcomi  30300  hvdistr1i  30304  hvsubdistr1i  30305  hvassi  30306  hvadd32i  30307  hvsubassi  30308  hvsub32i  30309  normlem0  30362  normlem8  30370  normlem9  30371  bcseqi  30373  polid2i  30410  hhph  30431  hlim0  30488  shscli  30570  shlessi  30630  shlej1i  30631  omlsilem  30655  shlubi  30668  h1de2i  30806  pjadjii  30927  pjaddii  30928  pjmulii  30930  pjdifnormii  30936  pjcji  30937  hoaddsubassi  31073  eigrei  31087  eigposi  31089  eigorthi  31090  adj0  31247  lnopeq0lem1  31258  lnopunilem1  31263  lnophmlem2  31270  nmcexi  31279  nmcopexi  31280  lnfn0i  31295  nmcfnexi  31304  mdexchi  31588  xppreima2  31876  dp2clq  32047  dp2lt  32051  dp2ltc  32053  dpexpp1  32074  dpmul  32079  dpmul4  32080  elxrge02  32098  xrge0adddir  32193  psgnid  32256  cnmsgn0g  32305  altgnsg  32308  xrnarchi  32330  xrge0slmod  32463  fermltlchr  32478  znfermltl  32479  ccfldextdgrr  32746  raddcn  32909  xrge0iifcnv  32913  xrge0iifiso  32915  xrge0iifhmeo  32916  xrge0iifhom  32917  xrge0iifmhm  32919  xrge0mulc1cn  32921  lmlimxrge0  32928  pnfneige0  32931  lmxrge0  32932  zringnm  32938  rezh  32951  qqh0  32964  qqh1  32965  qqhucn  32972  esumpinfval  33071  hashf2  33082  esumcvg  33084  br2base  33268  sxbrsigalem3  33271  dya2iocbrsiga  33274  dya2icobrsiga  33275  sxbrsigalem1  33284  sxbrsigalem2  33285  sxbrsigalem4  33286  sxbrsigalem5  33287  sxbrsiga  33289  ballotlem2  33487  ballotlem4  33497  ballotlemi1  33501  ballotth  33536  sgnclre  33538  signstf  33577  itgexpif  33618  chtvalz  33641  hgt750lemd  33660  hgt750lem  33663  tgoldbachgnn  33671  lfuhgr2  34109  subfacp1lem1  34170  subfacp1lem6  34176  kur14lem6  34202  cvmliftlem4  34279  satf0suc  34367  problem4  34653  quad3  34655  logi  34704  iexpire  34705  fununiq  34740  fvtransport  35004  gg-iimulcn  35169  bj-minftyccb  36106  taupilem2  36203  iccioo01  36208  1oequni2o  36249  finxp1o  36273  finxpreclem4  36275  cos2h  36479  tan2h  36480  poimirlem9  36497  poimirlem27  36515  poimirlem28  36516  ismblfin  36529  mbfposadd  36535  ftc1anclem5  36565  asindmre  36571  dvasin  36572  dvacos  36573  rrnval  36695  el3v  37086  dihjatcclem4  40292  lcmineqlem12  40905  sn-00idlem2  41272  sn-00id  41274  remul02  41278  rabren3dioph  41553  jm2.27dlem2  41749  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  expdioph  41762  arearect  41964  areaquad  41965  2omomeqom  42053  omnord1ex  42054  corclrcl  42458  iunrelexpuztr  42470  corcltrcl  42490  dffrege76  42690  k0004val0  42905  lhe4.4ex1a  43088  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  ax6e2ndeqALT  43692  sineq0ALT  43698  pnfel0pnf  44241  lptioo2cn  44361  limsup10ex  44489  liminf10ex  44490  icccncfext  44603  itgsin0pilem1  44666  itgsbtaddcnst  44698  stoweidlem13  44729  wallispilem2  44782  wallispilem4  44784  wallispi2lem1  44787  stirlinglem13  44802  dirkerper  44812  dirkertrigeqlem3  44816  dirkeritg  44818  dirkercncflem1  44819  dirkercncflem4  44822  fourierdlem42  44865  fourierdlem62  44884  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  sqwvfoura  44944  fourierswlem  44946  fouriersw  44947  smfmullem4  45510  fmtnoprmfac2lem1  46234  fmtno4prm  46243  3exp4mod41  46284  41prothprmlem2  46286  6gbe  46439  7gbow  46440  8gbe  46441  9gbo  46442  11gbo  46443  sbgoldbalt  46449  nnsum4primesevenALTV  46469  0nodd  46580  oddinmgm  46585  pzriprnglem13  46817  pzriprng1ALT  46820  2zrng0  46836  zlmodzxz0  47032  zlmodzxzequa  47177  zlmodzxzequap  47180  zlmodzxzldeplem3  47183  nnlog2ge0lt1  47252  blen1  47270  blen2  47271  nnolog2flm1  47276  ackval42  47382  ehl2eudisval0  47411  line2ylem  47437  i0oii  47552  io1ii  47553  sepfsepc  47560