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  3455  raltp  4669  rextp  4670  opthhausdorff  5477  funopg  6550  feq12i  6681  ftp  7129  caovass  7589  caovdi  7608  ordom  7852  mptexw  7931  ofmres  7963  sbcoteq1a  8030  mpoexw  8057  xpord3lem  8128  omopthlem1  8623  omopthlem2  8624  omopthi  8625  on2recsfn  8631  xpcomen  9032  snnen2o  9184  unfilem3  9256  hartogs  9497  card2on  9507  unwf  9763  inlresf1  9868  inrresf1  9870  tskwe  9903  alephsmo  10055  dfac4  10075  dfac2a  10083  ackbij1lem13  10184  axdc2lem  10401  axcclem  10410  ondomon  10516  cfpwsdom  10537  pwfseqlem2  10612  pwfseqlem3  10613  1lt2pi  10858  addassi  11184  mulassi  11185  adddii  11186  adddiri  11187  lttri  11300  lelttri  11301  ltletri  11302  letri  11303  ltadd2i  11305  mul02lem2  11351  addrid  11354  addcani  11367  addcan2i  11368  mul12i  11369  mul32i  11370  add12i  11397  add32i  11398  subaddi  11509  subadd2i  11510  subsub23i  11512  addsubassi  11513  addsubi  11514  subcani  11515  subcan2i  11516  pnncani  11517  subdii  11627  subdiri  11628  ltadd1i  11732  leadd1i  11733  leadd2i  11734  ltsubaddi  11735  lesubaddi  11736  ltsubadd2i  11737  lesubadd2i  11738  ltaddsubi  11739  mulcani  11817  div23i  11940  div11i  11941  3halfnz  12613  mpoaddex  12947  addex  12948  mpomulex  12949  mulex  12950  unirnioo  13410  ioorebas  13412  xnn0xrge0  13467  fldiv4lem1div2  13799  uzenom  13929  nnenom  13945  seqexw  13982  m1expcl2  14050  i4  14169  expnass  14173  faclbnd4lem1  14258  bcn1  14278  hashfxnn0  14302  ccat2s1p1  14594  ccat2s1p2  14595  cats1fvn  14824  cats1fv  14825  cats1cat  14827  cats2cat  14828  wrdlen3s3  14915  abs3difi  15376  0.999...  15847  bpoly3  16024  ef01bndlem  16152  cos1bnd  16155  cos2bnd  16156  sin4lt0  16163  rpnnen2lem3  16184  rpnnen2lem11  16192  rpnnen  16195  rexpen  16196  aleph1irr  16214  3dvdsdec  16302  3dvds2dec  16303  divalglem2  16365  ndvdsi  16382  flodddiv4  16385  gcdaddmlem  16494  bezout  16513  3lcm2e6woprm  16585  6lcm4e12  16586  lcmf0  16604  lcmf2a3a4e12  16617  dec2dvds  17034  modxai  17039  modsubi  17043  gcdi  17044  numexp2x  17049  2exp5  17056  2exp11  17060  0symgefmndeq  19324  pmtrprfval  19417  m1expaddsub  19428  0frgp  19709  staffval  20750  cnfldcj  21273  cnfldds  21276  cnfldfunALT  21279  cnfldcjOLD  21286  cnflddsOLD  21289  cnfldfunALTOLD  21292  xrsadd  21296  xrsmul  21297  xrsds  21326  cnmgpid  21346  nn0srg  21354  rge0srg  21355  zring0  21368  pzriprnglem13  21403  pzriprng1ALT  21406  fermltlchr  21439  cnmsgnsubg  21486  psgninv  21491  re0g  21521  ocvfval  21575  frlmbas  21664  mdetrlin  22489  mdetunilem9  22507  leordtval2  23099  iscnp2  23126  utop3cls  24139  nmfval  24476  nmoffn  24599  nmofval  24602  icccld  24654  addcnlem  24753  iimulcn  24834  iimulcnOLD  24835  icopnfhmeo  24841  iccpnfcnv  24842  iccpnfhmeo  24843  xrhmeo  24844  xrhmph  24845  oprpiece1res1  24849  oprpiece1res2  24850  ishtpy  24871  pcoass  24924  cnstrcvs  25041  cncvs  25045  recvs  25046  qcvs  25047  zclmncvs  25048  tcphex  25117  cnfldcusp  25257  resscdrg  25258  reust  25281  recusp  25282  vitalilem4  25512  vitalilem5  25513  mbfdm  25527  dveflem  25883  dvlipcn  25899  c1lip2  25903  dgrid  26170  iaa  26233  abelthlem3  26343  abelthlem5  26345  abelth  26351  efcn  26353  sinhalfpilem  26372  sincosq1lem  26406  sincosq4sgn  26410  tangtx  26414  sincos4thpi  26422  sincos6thpi  26425  pigt3  26427  pige3ALT  26429  cos0pilt1  26441  logi  26496  relogcn  26547  dvlog2lem  26561  dvlog2  26562  logtayl  26569  logtayl2  26571  cxpsqrtlem  26611  cxpsqrt  26612  2irrexpq  26640  cxpcn2  26656  cxpcn3  26658  logblog  26702  2logb9irr  26705  2logb3irr  26707  2logb9irrALT  26708  sqrt2cxp2logb9e3  26709  2irrexpqALT  26710  ang180lem1  26719  ang180lem2  26720  1cubrlem  26751  mcubic  26757  quart1lem  26765  quart1  26766  reasinsin  26806  atancj  26820  efiatan  26822  atantan  26833  atanbndlem  26835  atan1  26838  atancn  26846  atantayl2  26848  log2cnv  26854  log2tlbnd  26855  log2ublem1  26856  log2ublem2  26857  log2ub  26859  efrlim  26879  efrlimOLD  26880  scvxcvx  26896  1sgm2ppw  27111  ppiub  27115  bclbnd  27191  bposlem8  27202  lgsdir2lem1  27236  lgsdir2lem5  27240  lgseisenlem1  27286  lgseisenlem2  27287  lgsquadlem1  27291  chebbnd1  27383  dchrvmasumlem2  27409  norecfn  27853  norec2fn  27863  addsproplem2  27877  addsproplem6  27881  addsbdaylem  27923  negs1s  27933  negsproplem2  27935  mulsproplem2  28020  mulsproplem3  28021  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  mulsproplem13  28031  mulsproplem14  28032  0zs  28276  zseo  28308  twocut  28309  istrkg3ld  28388  trgcgrg  28442  ax5seglem7  28862  axlowdimlem6  28874  axlowdimlem8  28876  axlowdimlem11  28879  elntg2  28912  cusgrsizeindb1  29378  vtxdginducedm1  29471  0grrusgr  29507  erclwwlktr  29951  erclwwlkntr  30000  wlk2v2e  30086  upgr3v3e3cycl  30109  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  konigsberglem5  30185  ex-fl  30376  ex-mod  30378  ex-hash  30382  ex-lcm  30387  0vfval  30535  smcnlem  30626  lnocoi  30686  nmlno0lem  30722  nmblolbii  30728  blocnilem  30733  blocni  30734  cncph  30748  isph  30751  ip0i  30754  ip1ilem  30755  ip2i  30757  ipdirilem  30758  ipasslem7  30765  ipasslem8  30766  ipasslem9  30767  ipasslem10  30768  ipasslem11  30769  ip2dii  30773  pythi  30779  siilem1  30780  siilem2  30781  siii  30782  hvmulassi  30975  hvmulcomi  30976  hvdistr1i  30980  hvsubdistr1i  30981  hvassi  30982  hvadd32i  30983  hvsubassi  30984  hvsub32i  30985  normlem0  31038  normlem8  31046  normlem9  31047  bcseqi  31049  polid2i  31086  hhph  31107  hlim0  31164  shscli  31246  shlessi  31306  shlej1i  31307  omlsilem  31331  shlubi  31344  h1de2i  31482  pjadjii  31603  pjaddii  31604  pjmulii  31606  pjdifnormii  31612  pjcji  31613  hoaddsubassi  31749  eigrei  31763  eigposi  31765  eigorthi  31766  adj0  31923  lnopeq0lem1  31934  lnopunilem1  31939  lnophmlem2  31946  nmcexi  31955  nmcopexi  31956  lnfn0i  31971  nmcfnexi  31980  mdexchi  32264  xppreima2  32575  sgnclre  32757  dp2clq  32801  dp2lt  32805  dp2ltc  32807  dpexpp1  32828  dpmul  32833  dpmul4  32834  elxrge02  32852  xrge0adddir  32959  psgnid  33054  cnmsgn0g  33103  altgnsg  33106  xrnarchi  33138  xrge0slmod  33319  znfermltl  33337  ccfldextdgrr  33667  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  raddcn  33919  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhmeo  33926  xrge0iifhom  33927  xrge0iifmhm  33929  xrge0mulc1cn  33931  lmlimxrge0  33938  pnfneige0  33941  lmxrge0  33942  zringnm  33948  rezh  33959  qqh0  33974  qqh1  33975  qqhucn  33982  esumpinfval  34063  hashf2  34074  esumcvg  34076  br2base  34260  sxbrsigalem3  34263  dya2iocbrsiga  34266  dya2icobrsiga  34267  sxbrsigalem1  34276  sxbrsigalem2  34277  sxbrsigalem4  34278  sxbrsigalem5  34279  sxbrsiga  34281  ballotlem2  34480  ballotlem4  34490  ballotlemi1  34494  ballotth  34529  signstf  34557  itgexpif  34597  chtvalz  34620  hgt750lemd  34639  hgt750lem  34642  tgoldbachgnn  34650  lfuhgr2  35106  subfacp1lem1  35166  subfacp1lem6  35172  kur14lem6  35198  cvmliftlem4  35275  satf0suc  35363  problem4  35655  quad3  35657  iexpire  35722  fununiq  35756  fvtransport  36020  bj-minftyccb  37213  taupilem2  37310  iccioo01  37315  1oequni2o  37356  finxp1o  37380  finxpreclem4  37382  cos2h  37605  tan2h  37606  poimirlem9  37623  poimirlem27  37641  poimirlem28  37642  ismblfin  37655  mbfposadd  37661  ftc1anclem5  37691  asindmre  37697  dvasin  37698  dvacos  37699  rrnval  37821  dihjatcclem4  41415  lcmineqlem12  42028  fisdomnn  42232  subex  42235  absex  42236  cjex  42237  cxpi11d  42331  redvmptabs  42348  readvrec  42350  sn-00idlem2  42387  sn-00id  42389  remul02  42393  rabren3dioph  42803  jm2.27dlem2  42999  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  arearect  43204  areaquad  43205  2omomeqom  43292  omnord1ex  43293  corclrcl  43696  iunrelexpuztr  43708  corcltrcl  43728  dffrege76  43928  k0004val0  44143  lhe4.4ex1a  44318  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  ax6e2ndeqALT  44920  sineq0ALT  44926  nregmodelf1o  45005  pnfel0pnf  45526  lptioo2cn  45643  limsup10ex  45771  liminf10ex  45772  icccncfext  45885  itgsin0pilem1  45948  itgsbtaddcnst  45980  stoweidlem13  46011  wallispilem2  46064  wallispilem4  46066  wallispi2lem1  46069  stirlinglem13  46084  dirkerper  46094  dirkertrigeqlem3  46098  dirkeritg  46100  dirkercncflem1  46101  dirkercncflem4  46104  fourierdlem42  46147  fourierdlem62  46166  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  sqwvfoura  46226  fourierswlem  46228  fouriersw  46229  smfmullem4  46792  ceil5half3  47341  8mod5e3  47361  fmtnoprmfac2lem1  47567  fmtno4prm  47576  3exp4mod41  47617  41prothprmlem2  47619  6gbe  47772  7gbow  47773  8gbe  47774  9gbo  47775  11gbo  47776  sbgoldbalt  47782  nnsum4primesevenALTV  47802  usgrexmpl2nb0  48022  usgrexmpl2nb3  48025  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg3nbgrvtx1  48069  gpg5grlic  48084  0nodd  48158  oddinmgm  48163  2zrng0  48232  zlmodzxz0  48344  zlmodzxzequa  48485  zlmodzxzequap  48488  zlmodzxzldeplem3  48491  nnlog2ge0lt1  48555  blen1  48573  blen2  48574  nnolog2flm1  48579  ackval42  48685  ehl2eudisval0  48714  line2ylem  48740  i0oii  48908  io1ii  48909  sepfsepc  48916  rescofuf  49082  setc1ohomfval  49482  setc1ocofval  49483