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 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  3485  raltp  4709  rextp  4710  opthhausdorff  5526  funopg  6601  feq12i  6729  ftp  7176  caovass  7632  caovdi  7651  ordom  7896  mptexw  7975  ofmres  8007  sbcoteq1a  8074  mpoexw  8101  xpord3lem  8172  omopthlem1  8695  omopthlem2  8696  omopthi  8697  on2recsfn  8703  xpcomen  9101  snnen2o  9270  unfilem3  9342  hartogs  9581  card2on  9591  unwf  9847  inlresf1  9952  inrresf1  9954  tskwe  9987  alephsmo  10139  dfac4  10159  dfac2a  10167  ackbij1lem13  10268  axdc2lem  10485  axcclem  10494  ondomon  10600  cfpwsdom  10621  pwfseqlem2  10696  pwfseqlem3  10697  1lt2pi  10942  addassi  11268  mulassi  11269  adddii  11270  adddiri  11271  lttri  11384  lelttri  11385  ltletri  11386  letri  11387  ltadd2i  11389  mul02lem2  11435  addrid  11438  addcani  11451  addcan2i  11452  mul12i  11453  mul32i  11454  add12i  11481  add32i  11482  subaddi  11593  subadd2i  11594  subsub23i  11596  addsubassi  11597  addsubi  11598  subcani  11599  subcan2i  11600  pnncani  11601  subdii  11709  subdiri  11710  ltadd1i  11814  leadd1i  11815  leadd2i  11816  ltsubaddi  11817  lesubaddi  11818  ltsubadd2i  11819  lesubadd2i  11820  ltaddsubi  11821  mulcani  11899  div23i  12022  div11i  12023  1mhlfehlf  12482  halfpm6th  12484  3halfnz  12694  mpoaddex  13027  addex  13028  mpomulex  13029  mulex  13030  unirnioo  13485  ioorebas  13487  xnn0xrge0  13542  fldiv4lem1div2  13873  uzenom  14001  nnenom  14017  seqexw  14054  m1expcl2  14122  i4  14239  expnass  14243  faclbnd4lem1  14328  bcn1  14348  hashfxnn0  14372  ccat2s1p1  14663  ccat2s1p2  14664  cats1fvn  14893  cats1fv  14894  cats1cat  14896  cats2cat  14897  wrdlen3s3  14984  abs3difi  15444  0.999...  15913  bpoly3  16090  ef01bndlem  16216  cos1bnd  16219  cos2bnd  16220  sin4lt0  16227  rpnnen2lem3  16248  rpnnen2lem11  16256  rpnnen  16259  rexpen  16260  aleph1irr  16278  3dvdsdec  16365  3dvds2dec  16366  divalglem2  16428  ndvdsi  16445  flodddiv4  16448  gcdaddmlem  16557  bezout  16576  3lcm2e6woprm  16648  6lcm4e12  16649  lcmf0  16667  lcmf2a3a4e12  16680  dec2dvds  17096  modxai  17101  modsubi  17105  gcdi  17106  numexp2x  17112  2exp5  17119  2exp11  17123  0symgefmndeq  19425  pmtrprfval  19519  m1expaddsub  19530  0frgp  19811  staffval  20858  cnfldcj  21390  cnfldds  21393  cnfldfunALT  21396  cnfldcjOLD  21403  cnflddsOLD  21406  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  xrsadd  21414  xrsmul  21415  xrsds  21444  cnmgpid  21464  nn0srg  21472  rge0srg  21473  zring0  21486  pzriprnglem13  21521  pzriprng1ALT  21524  fermltlchr  21561  cnmsgnsubg  21612  psgninv  21617  re0g  21647  ocvfval  21701  frlmbas  21792  mdetrlin  22623  mdetunilem9  22641  leordtval2  23235  iscnp2  23262  utop3cls  24275  nmfval  24616  nmoffn  24747  nmofval  24750  icccld  24802  addcnlem  24899  iimulcn  24980  iimulcnOLD  24981  icopnfhmeo  24987  iccpnfcnv  24988  iccpnfhmeo  24989  xrhmeo  24990  xrhmph  24991  oprpiece1res1  24995  oprpiece1res2  24996  ishtpy  25017  pcoass  25070  cnstrcvs  25187  cncvs  25191  recvs  25192  recvsOLD  25193  qcvs  25194  zclmncvs  25195  tcphex  25264  cnfldcusp  25404  resscdrg  25405  reust  25428  recusp  25429  vitalilem4  25659  vitalilem5  25660  mbfdm  25674  dveflem  26031  dvlipcn  26047  c1lip2  26051  dgrid  26318  iaa  26381  abelthlem3  26491  abelthlem5  26493  abelth  26499  efcn  26501  sinhalfpilem  26519  sincosq1lem  26553  sincosq4sgn  26557  tangtx  26561  sincos4thpi  26569  sincos6thpi  26572  pigt3  26574  pige3ALT  26576  cos0pilt1  26588  logi  26643  relogcn  26694  dvlog2lem  26708  dvlog2  26709  logtayl  26716  logtayl2  26718  cxpsqrtlem  26758  cxpsqrt  26759  2irrexpq  26787  cxpcn2  26803  cxpcn3  26805  logblog  26849  2logb9irr  26852  2logb3irr  26854  2logb9irrALT  26855  sqrt2cxp2logb9e3  26856  2irrexpqALT  26857  ang180lem1  26866  ang180lem2  26867  1cubrlem  26898  mcubic  26904  quart1lem  26912  quart1  26913  reasinsin  26953  atancj  26967  efiatan  26969  atantan  26980  atanbndlem  26982  atan1  26985  atancn  26993  atantayl2  26995  log2cnv  27001  log2tlbnd  27002  log2ublem1  27003  log2ublem2  27004  log2ub  27006  efrlim  27026  efrlimOLD  27027  scvxcvx  27043  1sgm2ppw  27258  ppiub  27262  bclbnd  27338  bposlem8  27349  lgsdir2lem1  27383  lgsdir2lem5  27387  lgseisenlem1  27433  lgseisenlem2  27434  lgsquadlem1  27438  chebbnd1  27530  dchrvmasumlem2  27556  norecfn  27993  norec2fn  28003  addsproplem2  28017  addsproplem6  28021  addsbdaylem  28063  negs1s  28073  negsproplem2  28075  mulsproplem2  28157  mulsproplem3  28158  mulsproplem5  28160  mulsproplem6  28161  mulsproplem7  28162  mulsproplem8  28163  mulsproplem13  28168  mulsproplem14  28169  0zs  28388  zseo  28420  nohalf  28421  istrkg3ld  28483  trgcgrg  28537  ax5seglem7  28964  axlowdimlem6  28976  axlowdimlem8  28978  axlowdimlem11  28981  elntg2  29014  cusgrsizeindb1  29482  vtxdginducedm1  29575  0grrusgr  29611  erclwwlktr  30050  erclwwlkntr  30099  wlk2v2e  30185  upgr3v3e3cycl  30208  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  konigsberglem5  30284  ex-fl  30475  ex-mod  30477  ex-hash  30481  ex-lcm  30486  0vfval  30634  smcnlem  30725  lnocoi  30785  nmlno0lem  30821  nmblolbii  30827  blocnilem  30832  blocni  30833  cncph  30847  isph  30850  ip0i  30853  ip1ilem  30854  ip2i  30856  ipdirilem  30857  ipasslem7  30864  ipasslem8  30865  ipasslem9  30866  ipasslem10  30867  ipasslem11  30868  ip2dii  30872  pythi  30878  siilem1  30879  siilem2  30880  siii  30881  hvmulassi  31074  hvmulcomi  31075  hvdistr1i  31079  hvsubdistr1i  31080  hvassi  31081  hvadd32i  31082  hvsubassi  31083  hvsub32i  31084  normlem0  31137  normlem8  31145  normlem9  31146  bcseqi  31148  polid2i  31185  hhph  31206  hlim0  31263  shscli  31345  shlessi  31405  shlej1i  31406  omlsilem  31430  shlubi  31443  h1de2i  31581  pjadjii  31702  pjaddii  31703  pjmulii  31705  pjdifnormii  31711  pjcji  31712  hoaddsubassi  31848  eigrei  31862  eigposi  31864  eigorthi  31865  adj0  32022  lnopeq0lem1  32033  lnopunilem1  32038  lnophmlem2  32045  nmcexi  32054  nmcopexi  32055  lnfn0i  32070  nmcfnexi  32079  mdexchi  32363  xppreima2  32667  dp2clq  32847  dp2lt  32851  dp2ltc  32853  dpexpp1  32874  dpmul  32879  dpmul4  32880  elxrge02  32898  xrge0adddir  33005  psgnid  33099  cnmsgn0g  33148  altgnsg  33151  xrnarchi  33173  xrge0slmod  33355  znfermltl  33373  ccfldextdgrr  33696  raddcn  33889  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhmeo  33896  xrge0iifhom  33897  xrge0iifmhm  33899  xrge0mulc1cn  33901  lmlimxrge0  33908  pnfneige0  33911  lmxrge0  33912  zringnm  33918  rezh  33931  qqh0  33946  qqh1  33947  qqhucn  33954  esumpinfval  34053  hashf2  34064  esumcvg  34066  br2base  34250  sxbrsigalem3  34253  dya2iocbrsiga  34256  dya2icobrsiga  34257  sxbrsigalem1  34266  sxbrsigalem2  34267  sxbrsigalem4  34268  sxbrsigalem5  34269  sxbrsiga  34271  ballotlem2  34469  ballotlem4  34479  ballotlemi1  34483  ballotth  34518  sgnclre  34520  signstf  34559  itgexpif  34599  chtvalz  34622  hgt750lemd  34641  hgt750lem  34644  tgoldbachgnn  34652  lfuhgr2  35102  subfacp1lem1  35163  subfacp1lem6  35169  kur14lem6  35195  cvmliftlem4  35272  satf0suc  35360  problem4  35652  quad3  35654  iexpire  35714  fununiq  35749  fvtransport  36013  bj-minftyccb  37207  taupilem2  37304  iccioo01  37309  1oequni2o  37350  finxp1o  37374  finxpreclem4  37376  cos2h  37597  tan2h  37598  poimirlem9  37615  poimirlem27  37633  poimirlem28  37634  ismblfin  37647  mbfposadd  37653  ftc1anclem5  37683  asindmre  37689  dvasin  37690  dvacos  37691  rrnval  37813  dihjatcclem4  41403  lcmineqlem12  42021  fisdomnn  42263  subex  42266  absex  42267  cjex  42268  cxpi11d  42357  redvmptabs  42368  readvrec  42370  sn-00idlem2  42405  sn-00id  42407  remul02  42411  rabren3dioph  42802  jm2.27dlem2  42998  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  arearect  43203  areaquad  43204  2omomeqom  43292  omnord1ex  43293  corclrcl  43696  iunrelexpuztr  43708  corcltrcl  43728  dffrege76  43928  k0004val0  44143  lhe4.4ex1a  44324  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  ax6e2ndeqALT  44928  sineq0ALT  44934  pnfel0pnf  45480  lptioo2cn  45600  limsup10ex  45728  liminf10ex  45729  icccncfext  45842  itgsin0pilem1  45905  itgsbtaddcnst  45937  stoweidlem13  45968  wallispilem2  46021  wallispilem4  46023  wallispi2lem1  46026  stirlinglem13  46041  dirkerper  46051  dirkertrigeqlem3  46055  dirkeritg  46057  dirkercncflem1  46058  dirkercncflem4  46061  fourierdlem42  46104  fourierdlem62  46123  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  sqwvfoura  46183  fourierswlem  46185  fouriersw  46186  smfmullem4  46749  ceil5half3  47279  fmtnoprmfac2lem1  47490  fmtno4prm  47499  3exp4mod41  47540  41prothprmlem2  47542  6gbe  47695  7gbow  47696  8gbe  47697  9gbo  47698  11gbo  47699  sbgoldbalt  47705  nnsum4primesevenALTV  47725  usgrexmpl2nb0  47925  usgrexmpl2nb3  47928  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  gpg5grlic  47974  0nodd  48013  oddinmgm  48018  2zrng0  48087  zlmodzxz0  48200  zlmodzxzequa  48341  zlmodzxzequap  48344  zlmodzxzldeplem3  48347  nnlog2ge0lt1  48415  blen1  48433  blen2  48434  nnolog2flm1  48439  ackval42  48545  ehl2eudisval0  48574  line2ylem  48600  i0oii  48715  io1ii  48716  sepfsepc  48723