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  3444  raltp  4657  rextp  4658  opthhausdorff  5460  funopg  6516  feq12i  6645  ftp  7091  caovass  7549  caovdi  7568  ordom  7809  mptexw  7888  ofmres  7919  sbcoteq1a  7986  mpoexw  8013  xpord3lem  8082  omopthlem1  8577  omopthlem2  8578  omopthi  8579  on2recsfn  8585  xpcomen  8985  snnen2o  9134  unfilem3  9196  hartogs  9436  card2on  9446  unwf  9706  inlresf1  9811  inrresf1  9813  tskwe  9846  alephsmo  9996  dfac4  10016  dfac2a  10024  ackbij1lem13  10125  axdc2lem  10342  axcclem  10351  ondomon  10457  cfpwsdom  10478  pwfseqlem2  10553  pwfseqlem3  10554  1lt2pi  10799  addassi  11125  mulassi  11126  adddii  11127  adddiri  11128  lttri  11242  lelttri  11243  ltletri  11244  letri  11245  ltadd2i  11247  mul02lem2  11293  addrid  11296  addcani  11309  addcan2i  11310  mul12i  11311  mul32i  11312  add12i  11339  add32i  11340  subaddi  11451  subadd2i  11452  subsub23i  11454  addsubassi  11455  addsubi  11456  subcani  11457  subcan2i  11458  pnncani  11459  subdii  11569  subdiri  11570  ltadd1i  11674  leadd1i  11675  leadd2i  11676  ltsubaddi  11677  lesubaddi  11678  ltsubadd2i  11679  lesubadd2i  11680  ltaddsubi  11681  mulcani  11759  div23i  11882  div11i  11883  3halfnz  12555  mpoaddex  12889  addex  12890  mpomulex  12891  mulex  12892  unirnioo  13352  ioorebas  13354  xnn0xrge0  13409  fldiv4lem1div2  13741  uzenom  13871  nnenom  13887  seqexw  13924  m1expcl2  13992  i4  14111  expnass  14115  faclbnd4lem1  14200  bcn1  14220  hashfxnn0  14244  ccat2s1p1  14536  ccat2s1p2  14537  cats1fvn  14765  cats1fv  14766  cats1cat  14768  cats2cat  14769  wrdlen3s3  14856  abs3difi  15317  0.999...  15788  bpoly3  15965  ef01bndlem  16093  cos1bnd  16096  cos2bnd  16097  sin4lt0  16104  rpnnen2lem3  16125  rpnnen2lem11  16133  rpnnen  16136  rexpen  16137  aleph1irr  16155  3dvdsdec  16243  3dvds2dec  16244  divalglem2  16306  ndvdsi  16323  flodddiv4  16326  gcdaddmlem  16435  bezout  16454  3lcm2e6woprm  16526  6lcm4e12  16527  lcmf0  16545  lcmf2a3a4e12  16558  dec2dvds  16975  modxai  16980  modsubi  16984  gcdi  16985  numexp2x  16990  2exp5  16997  2exp11  17001  0symgefmndeq  19273  pmtrprfval  19366  m1expaddsub  19377  0frgp  19658  staffval  20726  cnfldcj  21270  cnfldds  21273  cnfldfunALT  21276  cnfldcjOLD  21283  cnflddsOLD  21286  cnfldfunALTOLD  21289  xrsadd  21292  xrsmul  21293  xrsds  21316  cnmgpid  21336  nn0srg  21344  rge0srg  21345  zring0  21365  pzriprnglem13  21400  pzriprng1ALT  21403  fermltlchr  21436  cnmsgnsubg  21484  psgninv  21489  re0g  21519  ocvfval  21573  frlmbas  21662  mdetrlin  22487  mdetunilem9  22505  leordtval2  23097  iscnp2  23124  utop3cls  24137  nmfval  24474  nmoffn  24597  nmofval  24600  icccld  24652  addcnlem  24751  iimulcn  24832  iimulcnOLD  24833  icopnfhmeo  24839  iccpnfcnv  24840  iccpnfhmeo  24841  xrhmeo  24842  xrhmph  24843  oprpiece1res1  24847  oprpiece1res2  24848  ishtpy  24869  pcoass  24922  cnstrcvs  25039  cncvs  25043  recvs  25044  qcvs  25045  zclmncvs  25046  tcphex  25115  cnfldcusp  25255  resscdrg  25256  reust  25279  recusp  25280  vitalilem4  25510  vitalilem5  25511  mbfdm  25525  dveflem  25881  dvlipcn  25897  c1lip2  25901  dgrid  26168  iaa  26231  abelthlem3  26341  abelthlem5  26343  abelth  26349  efcn  26351  sinhalfpilem  26370  sincosq1lem  26404  sincosq4sgn  26408  tangtx  26412  sincos4thpi  26420  sincos6thpi  26423  pigt3  26425  pige3ALT  26427  cos0pilt1  26439  logi  26494  relogcn  26545  dvlog2lem  26559  dvlog2  26560  logtayl  26567  logtayl2  26569  cxpsqrtlem  26609  cxpsqrt  26610  2irrexpq  26638  cxpcn2  26654  cxpcn3  26656  logblog  26700  2logb9irr  26703  2logb3irr  26705  2logb9irrALT  26706  sqrt2cxp2logb9e3  26707  2irrexpqALT  26708  ang180lem1  26717  ang180lem2  26718  1cubrlem  26749  mcubic  26755  quart1lem  26763  quart1  26764  reasinsin  26804  atancj  26818  efiatan  26820  atantan  26831  atanbndlem  26833  atan1  26836  atancn  26844  atantayl2  26846  log2cnv  26852  log2tlbnd  26853  log2ublem1  26854  log2ublem2  26855  log2ub  26857  efrlim  26877  efrlimOLD  26878  scvxcvx  26894  1sgm2ppw  27109  ppiub  27113  bclbnd  27189  bposlem8  27200  lgsdir2lem1  27234  lgsdir2lem5  27238  lgseisenlem1  27284  lgseisenlem2  27285  lgsquadlem1  27289  chebbnd1  27381  dchrvmasumlem2  27407  norecfn  27860  norec2fn  27870  addsproplem2  27884  addsproplem6  27888  addsbdaylem  27930  negs1s  27940  negsproplem2  27942  mulsproplem2  28027  mulsproplem3  28028  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  mulsproplem13  28038  mulsproplem14  28039  0zs  28283  zseo  28316  twocut  28317  istrkg3ld  28410  trgcgrg  28464  ax5seglem7  28884  axlowdimlem6  28896  axlowdimlem8  28898  axlowdimlem11  28901  elntg2  28934  cusgrsizeindb1  29400  vtxdginducedm1  29493  0grrusgr  29529  erclwwlktr  29970  erclwwlkntr  30019  wlk2v2e  30105  upgr3v3e3cycl  30128  konigsberglem1  30200  konigsberglem2  30201  konigsberglem3  30202  konigsberglem5  30204  ex-fl  30395  ex-mod  30397  ex-hash  30401  ex-lcm  30406  0vfval  30554  smcnlem  30645  lnocoi  30705  nmlno0lem  30741  nmblolbii  30747  blocnilem  30752  blocni  30753  cncph  30767  isph  30770  ip0i  30773  ip1ilem  30774  ip2i  30776  ipdirilem  30777  ipasslem7  30784  ipasslem8  30785  ipasslem9  30786  ipasslem10  30787  ipasslem11  30788  ip2dii  30792  pythi  30798  siilem1  30799  siilem2  30800  siii  30801  hvmulassi  30994  hvmulcomi  30995  hvdistr1i  30999  hvsubdistr1i  31000  hvassi  31001  hvadd32i  31002  hvsubassi  31003  hvsub32i  31004  normlem0  31057  normlem8  31065  normlem9  31066  bcseqi  31068  polid2i  31105  hhph  31126  hlim0  31183  shscli  31265  shlessi  31325  shlej1i  31326  omlsilem  31350  shlubi  31363  h1de2i  31501  pjadjii  31622  pjaddii  31623  pjmulii  31625  pjdifnormii  31631  pjcji  31632  hoaddsubassi  31768  eigrei  31782  eigposi  31784  eigorthi  31785  adj0  31942  lnopeq0lem1  31953  lnopunilem1  31958  lnophmlem2  31965  nmcexi  31974  nmcopexi  31975  lnfn0i  31990  nmcfnexi  31999  mdexchi  32283  xppreima2  32602  sgnclre  32786  dp2clq  32830  dp2lt  32834  dp2ltc  32836  dpexpp1  32857  dpmul  32862  dpmul4  32863  elxrge02  32881  xrge0adddir  32981  psgnid  33048  cnmsgn0g  33097  altgnsg  33100  xrnarchi  33135  xrge0slmod  33294  znfermltl  33312  ccfldextdgrr  33655  cos9thpiminplylem4  33768  cos9thpiminplylem5  33769  raddcn  33912  xrge0iifcnv  33916  xrge0iifiso  33918  xrge0iifhmeo  33919  xrge0iifhom  33920  xrge0iifmhm  33922  xrge0mulc1cn  33924  lmlimxrge0  33931  pnfneige0  33934  lmxrge0  33935  zringnm  33941  rezh  33952  qqh0  33967  qqh1  33968  qqhucn  33975  esumpinfval  34056  hashf2  34067  esumcvg  34069  br2base  34253  sxbrsigalem3  34256  dya2iocbrsiga  34259  dya2icobrsiga  34260  sxbrsigalem1  34269  sxbrsigalem2  34270  sxbrsigalem4  34271  sxbrsigalem5  34272  sxbrsiga  34274  ballotlem2  34473  ballotlem4  34483  ballotlemi1  34487  ballotth  34522  signstf  34550  itgexpif  34590  chtvalz  34613  hgt750lemd  34632  hgt750lem  34635  tgoldbachgnn  34643  lfuhgr2  35112  subfacp1lem1  35172  subfacp1lem6  35178  kur14lem6  35204  cvmliftlem4  35281  satf0suc  35369  problem4  35661  quad3  35663  iexpire  35728  fununiq  35762  fvtransport  36026  bj-minftyccb  37219  taupilem2  37316  iccioo01  37321  1oequni2o  37362  finxp1o  37386  finxpreclem4  37388  cos2h  37611  tan2h  37612  poimirlem9  37629  poimirlem27  37647  poimirlem28  37648  ismblfin  37661  mbfposadd  37667  ftc1anclem5  37697  asindmre  37703  dvasin  37704  dvacos  37705  rrnval  37827  dihjatcclem4  41420  lcmineqlem12  42033  fisdomnn  42237  subex  42240  absex  42241  cjex  42242  cxpi11d  42336  redvmptabs  42353  readvrec  42355  sn-00idlem2  42392  sn-00id  42394  remul02  42398  rabren3dioph  42808  jm2.27dlem2  43003  rmydioph  43007  rmxdioph  43009  expdiophlem2  43015  expdioph  43016  arearect  43208  areaquad  43209  2omomeqom  43296  omnord1ex  43297  corclrcl  43700  iunrelexpuztr  43712  corcltrcl  43732  dffrege76  43932  k0004val0  44147  lhe4.4ex1a  44322  binomcxplemdvbinom  44346  binomcxplemnotnn0  44349  ax6e2ndeqALT  44924  sineq0ALT  44930  nregmodelf1o  45009  pnfel0pnf  45529  lptioo2cn  45646  limsup10ex  45774  liminf10ex  45775  icccncfext  45888  itgsin0pilem1  45951  itgsbtaddcnst  45983  stoweidlem13  46014  wallispilem2  46067  wallispilem4  46069  wallispi2lem1  46072  stirlinglem13  46087  dirkerper  46097  dirkertrigeqlem3  46101  dirkeritg  46103  dirkercncflem1  46104  dirkercncflem4  46107  fourierdlem42  46150  fourierdlem62  46169  fourierdlem102  46209  fourierdlem103  46210  fourierdlem104  46211  fourierdlem114  46221  sqwvfoura  46229  fourierswlem  46231  fouriersw  46232  smfmullem4  46795  ceil5half3  47344  8mod5e3  47364  fmtnoprmfac2lem1  47570  fmtno4prm  47579  3exp4mod41  47620  41prothprmlem2  47622  6gbe  47775  7gbow  47776  8gbe  47777  9gbo  47778  11gbo  47779  sbgoldbalt  47785  nnsum4primesevenALTV  47805  usgrexmpl2nb0  48035  usgrexmpl2nb3  48038  gpg3nbgrvtx0  48080  gpg3nbgrvtx0ALT  48081  gpg3nbgrvtx1  48082  gpg5grlim  48097  gpg5grlic  48098  0nodd  48174  oddinmgm  48179  2zrng0  48248  zlmodzxz0  48360  zlmodzxzequa  48501  zlmodzxzequap  48504  zlmodzxzldeplem3  48507  nnlog2ge0lt1  48571  blen1  48589  blen2  48590  nnolog2flm1  48595  ackval42  48701  ehl2eudisval0  48730  line2ylem  48756  i0oii  48924  io1ii  48925  sepfsepc  48932  rescofuf  49098  setc1ohomfval  49498  setc1ocofval  49499