Theorem mp3an 1490

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  el3v  3461  raltp  4669  rextp  4670  opthhausdorff  5498  funopg  6571  feq12i  6699  ftp  7157  caovass  7617  caovdi  7636  ordom  7875  mptexw  7953  ofmres  7984  sbcoteq1a  8051  mpoexw  8080  xpord3lem  8150  omopthlem1  8650  omopthlem2  8651  omopthi  8652  on2recsfn  8658  xpcomen  9069  snnen2o  9218  unfilem3  9280  hartogs  9519  card2on  9529  unwf  9795  inlresf1  9923  inrresf1  9925  tskwe  9958  alephsmo  10108  dfac4  10128  dfac2a  10135  ackbij1lem13  10236  axdc2lem  10453  axcclem  10462  ondomon  10574  cfpwsdom  10596  pwfseqlem2  10671  pwfseqlem3  10672  1lt2pi  10917  addassi  11246  mulassi  11247  adddii  11248  adddiri  11249  lttri  11363  lelttri  11364  ltletri  11365  letri  11366  ltadd2i  11368  mul02lem2  11414  addrid  11417  addcani  11430  addcan2i  11431  mul12i  11432  mul32i  11433  add12i  11460  add32i  11461  subaddi  11572  subadd2i  11573  subsub23i  11575  addsubassi  11576  addsubi  11577  subcani  11578  subcan2i  11579  pnncani  11580  subdii  11690  subdiri  11691  ltadd1i  11795  leadd1i  11796  leadd2i  11797  ltsubaddi  11798  lesubaddi  11799  ltsubadd2i  11800  lesubadd2i  11801  ltaddsubi  11802  mulcani  11880  div23i  12000  div11i  12001  3halfnz  12703  mpoaddex  13040  addex  13041  mpomulex  13042  mulex  13043  unirnioo  13504  ioorebas  13506  xnn0xrge0  13561  fldiv4lem1div2  13900  uzenom  14030  nnenom  14046  seqexw  14083  m1expcl2  14151  i4  14270  expnass  14274  faclbnd4lem1  14359  bcn1  14379  hashfxnn0  14403  ccat2s1p1  14699  ccat2s1p2  14700  cats1fvn  14931  cats1fv  14932  cats1cat  14934  cats2cat  14935  wrdlen3s3  15022  sgnrn  15173  sgnclre  15177  abs3difi  15499  0.999...  15972  bpoly3  16148  ef01bndlem  16276  cos1bnd  16279  cos2bnd  16280  sin4lt0  16287  rpnnen2lem3  16308  rpnnen2lem11  16316  rpnnen  16319  rexpen  16320  aleph1irr  16338  3dvdsdec  16426  3dvds2dec  16427  divalglem2  16489  ndvdsi  16506  flodddiv4  16509  gcdaddmlem  16618  bezout  16637  3lcm2e6woprm  16709  6lcm4e12  16710  lcmf0  16728  lcmf2a3a4e12  16741  dec2dvds  17159  modxai  17164  modsubi  17168  gcdi  17169  numexp2x  17174  2exp5  17181  2exp11  17185  ex-chn2  18730  degenmgmnfn  19050  degenmgm  19051  degenmgm2opdm  19052  degenmgm2  19054  0symgefmndeq  19522  pmtrprfval  19615  m1expaddsub  19626  0frgp  19907  staffval  21008  cnfldcj  21595  cnfldds  21598  cnfldfunALT  21601  xrsadd  21604  xrsmul  21605  xrsds  21624  cnmgpid  21643  nn0srg  21651  rge0srg  21652  zring0  21672  pzriprnglem13  21707  pzriprng1ALT  21710  fermltlchr  21743  cnmsgnsubg  21791  psgninv  21796  re0g  21826  ocvfval  21880  frlmbas  21969  mdetrlin  22825  mdetunilem9  22843  leordtval2  23438  iscnp2  23465  utop3cls  24478  nmfval  24815  nmoffn  24938  nmofval  24941  icccld  24993  addcnlem  25092  iimulcn  25167  icopnfhmeo  25172  iccpnfcnv  25173  iccpnfhmeo  25174  xrhmeo  25175  xrhmph  25176  oprpiece1res1  25180  oprpiece1res2  25181  ishtpy  25201  pcoass  25253  cnstrcvs  25370  cncvs  25374  recvs  25375  qcvs  25376  zclmncvs  25377  tcphex  25446  cnfldcusp  25586  resscdrg  25587  reust  25610  recusp  25611  vitalilem4  25840  vitalilem5  25841  mbfdm  25855  dveflem  26208  dvlipcn  26223  c1lip2  26227  dgrid  26491  iaa  26558  abelthlem3  26666  abelthlem5  26668  abelth  26674  efcn  26676  sinhalfpilem  26698  sincosq1lem  26732  sincosq4sgn  26736  tangtx  26740  sincos4thpi  26748  sincos6thpi  26751  pigt3  26753  pige3ALT  26755  cos0pilt1  26767  logi  26822  relogcn  26873  dvlog2lem  26887  dvlog2  26888  logtayl  26895  logtayl2  26897  cxpsqrtlem  26937  cxpsqrt  26938  2irrexpq  26966  cxpcn2  26981  cxpcn3  26983  logblog  27027  2logb9irr  27030  2logb3irr  27032  2logb9irrALT  27033  sqrt2cxp2logb9e3  27034  2irrexpqALT  27035  ang180lem1  27044  ang180lem2  27045  1cubrlem  27076  mcubic  27082  quart1lem  27090  quart1  27091  reasinsin  27131  atancj  27145  efiatan  27147  atantan  27158  atanbndlem  27160  atan1  27163  atancn  27171  atantayl2  27173  log2cnv  27179  log2tlbnd  27180  log2ublem1  27181  log2ublem2  27182  log2ub  27184  efrlim  27204  scvxcvx  27220  1sgm2ppw  27434  ppiub  27438  bclbnd  27514  bposlem8  27525  lgsdir2lem1  27559  lgsdir2lem5  27563  lgseisenlem1  27609  lgseisenlem2  27610  lgsquadlem1  27614  chebbnd1  27706  dchrvmasumlem2  27732  norecfn  28209  norec2fn  28219  addsproplem2  28233  addsproplem6  28237  addbdaylem  28280  neg1s  28290  negsproplem2  28292  mulsproplem2  28380  mulsproplem3  28381  mulsproplem5  28383  mulsproplem6  28384  mulsproplem7  28385  mulsproplem8  28386  mulsproplem13  28391  mulsproplem14  28392  0zs  28651  zseo  28685  twocut  28686  bdaypw2n0bndlem  28726  bdaypw2bnd  28728  bdayfinbndlem1  28730  z12bdaylem2  28734  istrkg3ld  28800  trgcgrg  28855  ax5seglem7  29378  axlowdimlem6  29390  axlowdimlem8  29392  axlowdimlem11  29395  elntg2  29428  lfuhgr2  29592  cusgrsizeindb1  29896  vtxdginducedm1  29989  0grrusgr  30025  erclwwlktr  30478  erclwwlkntr  30527  wlk2v2e  30623  upgr3v3e3cycl  30646  konigsberglem1  30718  konigsberglem2  30719  konigsberglem3  30720  konigsberglem5  30722  ex-fl  30913  ex-mod  30915  ex-hash  30919  ex-lcm  30924  0vfval  31073  smcnlem  31164  lnocoi  31224  nmlno0lem  31260  nmblolbii  31266  blocnilem  31271  blocni  31272  cncph  31286  isph  31289  ip0i  31292  ip1ilem  31293  ip2i  31295  ipdirilem  31296  ipasslem7  31303  ipasslem8  31304  ipasslem9  31305  ipasslem10  31306  ipasslem11  31307  ip2dii  31311  pythi  31317  siilem1  31318  siilem2  31319  siii  31320  hvmulassi  31513  hvmulcomi  31514  hvdistr1i  31518  hvsubdistr1i  31519  hvassi  31520  hvadd32i  31521  hvsubassi  31522  hvsub32i  31523  normlem0  31576  normlem8  31584  normlem9  31585  bcseqi  31587  polid2i  31624  hhph  31645  hlim0  31702  shscli  31784  shlessi  31844  shlej1i  31845  omlsilem  31869  shlubi  31882  h1de2i  32020  pjadjii  32141  pjaddii  32142  pjmulii  32144  pjdifnormii  32150  pjcji  32151  hoaddsubassi  32287  eigrei  32301  eigposi  32303  eigorthi  32304  adj0  32461  lnopeq0lem1  32472  lnopunilem1  32477  lnophmlem2  32484  nmcexi  32493  nmcopexi  32494  lnfn0i  32509  nmcfnexi  32518  mdexchi  32802  xppreima2  33111  dp2clq  33313  dp2lt  33317  dp2ltc  33319  dpexpp1  33340  dpmul  33345  dpmul4  33346  elxrge02  33364  xrge0adddir  33445  psgnid  33524  cnmsgn0g  33573  altgnsg  33576  xrnarchi  33611  xrge0slmod  33775  znfermltl  33788  ccfldextdgrr  34169  cos9thpiminplylem4  34282  cos9thpiminplylem5  34283  raddcn  34426  xrge0iifcnv  34430  xrge0iifiso  34432  xrge0iifhmeo  34433  xrge0iifhom  34434  xrge0iifmhm  34436  xrge0mulc1cn  34438  lmlimxrge0  34445  pnfneige0  34448  lmxrge0  34449  zringnm  34455  rezh  34466  qqh0  34481  qqh1  34482  qqhucn  34489  esumpinfval  34570  hashf2  34581  esumcvg  34583  br2base  34767  sxbrsigalem3  34770  dya2iocbrsiga  34773  dya2icobrsiga  34774  sxbrsigalem1  34783  sxbrsigalem2  34784  sxbrsigalem4  34785  sxbrsigalem5  34786  sxbrsiga  34788  ballotlem2  34987  ballotlem4  34997  ballotlemi1  35001  ballotth  35036  signstf  35061  itgexpif  35101  chtvalz  35124  hgt750lemd  35143  hgt750lem  35146  tgoldbachgnn  35154  subfacp1lem1  35745  subfacp1lem6  35751  kur14lem6  35777  cvmliftlem4  35854  satf0suc  35942  problem4  36234  quad3  36236  iexpire  36301  fununiq  36335  fvtransport  36599  ttcid  37098  dfttc2g  37112  bj-minftyccb  37964  taupilem2  38061  iccioo01  38068  1oequni2o  38109  finxp1o  38133  finxpreclem4  38135  cos2h  38352  tan2h  38353  poimirlem9  38365  poimirlem27  38383  poimirlem28  38384  ismblfin  38397  mbfposadd  38403  ftc1anclem5  38433  asindmre  38439  dvasin  38440  dvacos  38441  rrnval  38564  dihjatcclem4  42281  lcmineqlem12  42893  fisdomnn  43098  subex  43101  absex  43102  cjex  43103  cxpi11d  43205  redvmptabs  43222  readvrec  43224  sn-00idlem2  43261  sn-00id  43263  remul02  43267  rabren3dioph  43643  jm2.27dlem2  43838  rmydioph  43842  rmxdioph  43844  expdiophlem2  43850  expdioph  43851  arearect  44043  areaquad  44044  2omomeqom  44131  omnord1ex  44132  corclrcl  44534  iunrelexpuztr  44546  corcltrcl  44566  dffrege76  44766  k0004val0  44981  lhe4.4ex1a  45140  binomcxplemdvbinom  45164  binomcxplemnotnn0  45167  ax6e2ndeqALT  45740  sineq0ALT  45746  nregmodelf1o  45825  pnfel0pnf  46345  lptioo2cn  46460  limsup10ex  46588  liminf10ex  46589  icccncfext  46702  itgsin0pilem1  46765  itgsbtaddcnst  46797  stoweidlem13  46828  wallispilem2  46881  wallispilem4  46883  wallispi2lem1  46886  stirlinglem13  46901  dirkerper  46911  dirkertrigeqlem3  46915  dirkeritg  46917  dirkercncflem1  46918  dirkercncflem4  46921  fourierdlem42  46964  fourierdlem62  46983  fourierdlem102  47023  fourierdlem103  47024  fourierdlem104  47025  fourierdlem114  47035  sqwvfoura  47043  fourierswlem  47045  fouriersw  47046  smfmullem4  47609  sqrtnnaa  47718  sqrtnzqaa  47719  goldpolyfactor  47732  goldracos5teq  47737  goldratmolem2  47738  goldratval  47741  sqrtnpoly  47748  ceil5half3  48221  8mod5e3  48241  fmtnoprmfac2lem1  48456  fmtno4prm  48465  3exp4mod41  48506  41prothprmlem2  48508  ppivalnn4  48517  6gbe  48674  7gbow  48675  8gbe  48676  9gbo  48677  11gbo  48678  sbgoldbalt  48684  nnsum4primesevenALTV  48704  usgrexmpl2nb0  48934  usgrexmpl2nb3  48937  gpg3nbgrvtx0  48979  gpg3nbgrvtx0ALT  48980  gpg3nbgrvtx1  48981  gpg5grlim  48996  gpg5grlic  48997  0nodd  49072  oddinmgm  49077  2zrng0  49146  zlmodzxz0  49273  zlmodzxzequa  49413  zlmodzxzequap  49416  zlmodzxzldeplem3  49419  nnlog2ge0lt1  49483  blen1  49501  blen2  49502  nnolog2flm1  49507  ackval42  49613  ehl2eudisval0  49642  line2ylem  49668  i0oii  49833  io1ii  49834  sepfsepc  49841  rescofuf  50006  setc1ohomfval  50406  setc1ocofval  50407