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  3452  raltp  4665  rextp  4666  opthhausdorff  5472  funopg  6534  feq12i  6663  ftp  7111  caovass  7569  caovdi  7588  ordom  7832  mptexw  7911  ofmres  7942  sbcoteq1a  8009  mpoexw  8036  xpord3lem  8105  omopthlem1  8600  omopthlem2  8601  omopthi  8602  on2recsfn  8608  xpcomen  9009  snnen2o  9161  unfilem3  9232  hartogs  9473  card2on  9483  unwf  9741  inlresf1  9846  inrresf1  9848  tskwe  9881  alephsmo  10033  dfac4  10053  dfac2a  10061  ackbij1lem13  10162  axdc2lem  10379  axcclem  10388  ondomon  10494  cfpwsdom  10515  pwfseqlem2  10590  pwfseqlem3  10591  1lt2pi  10836  addassi  11162  mulassi  11163  adddii  11164  adddiri  11165  lttri  11278  lelttri  11279  ltletri  11280  letri  11281  ltadd2i  11283  mul02lem2  11329  addrid  11332  addcani  11345  addcan2i  11346  mul12i  11347  mul32i  11348  add12i  11375  add32i  11376  subaddi  11487  subadd2i  11488  subsub23i  11490  addsubassi  11491  addsubi  11492  subcani  11493  subcan2i  11494  pnncani  11495  subdii  11605  subdiri  11606  ltadd1i  11710  leadd1i  11711  leadd2i  11712  ltsubaddi  11713  lesubaddi  11714  ltsubadd2i  11715  lesubadd2i  11716  ltaddsubi  11717  mulcani  11795  div23i  11918  div11i  11919  3halfnz  12591  mpoaddex  12925  addex  12926  mpomulex  12927  mulex  12928  unirnioo  13388  ioorebas  13390  xnn0xrge0  13445  fldiv4lem1div2  13777  uzenom  13907  nnenom  13923  seqexw  13960  m1expcl2  14028  i4  14147  expnass  14151  faclbnd4lem1  14236  bcn1  14256  hashfxnn0  14280  ccat2s1p1  14572  ccat2s1p2  14573  cats1fvn  14801  cats1fv  14802  cats1cat  14804  cats2cat  14805  wrdlen3s3  14892  abs3difi  15353  0.999...  15824  bpoly3  16001  ef01bndlem  16129  cos1bnd  16132  cos2bnd  16133  sin4lt0  16140  rpnnen2lem3  16161  rpnnen2lem11  16169  rpnnen  16172  rexpen  16173  aleph1irr  16191  3dvdsdec  16279  3dvds2dec  16280  divalglem2  16342  ndvdsi  16359  flodddiv4  16362  gcdaddmlem  16471  bezout  16490  3lcm2e6woprm  16562  6lcm4e12  16563  lcmf0  16581  lcmf2a3a4e12  16594  dec2dvds  17011  modxai  17016  modsubi  17020  gcdi  17021  numexp2x  17026  2exp5  17033  2exp11  17037  0symgefmndeq  19309  pmtrprfval  19402  m1expaddsub  19413  0frgp  19694  staffval  20762  cnfldcj  21306  cnfldds  21309  cnfldfunALT  21312  cnfldcjOLD  21319  cnflddsOLD  21322  cnfldfunALTOLD  21325  xrsadd  21328  xrsmul  21329  xrsds  21352  cnmgpid  21372  nn0srg  21380  rge0srg  21381  zring0  21401  pzriprnglem13  21436  pzriprng1ALT  21439  fermltlchr  21472  cnmsgnsubg  21520  psgninv  21525  re0g  21555  ocvfval  21609  frlmbas  21698  mdetrlin  22523  mdetunilem9  22541  leordtval2  23133  iscnp2  23160  utop3cls  24173  nmfval  24510  nmoffn  24633  nmofval  24636  icccld  24688  addcnlem  24787  iimulcn  24868  iimulcnOLD  24869  icopnfhmeo  24875  iccpnfcnv  24876  iccpnfhmeo  24877  xrhmeo  24878  xrhmph  24879  oprpiece1res1  24883  oprpiece1res2  24884  ishtpy  24905  pcoass  24958  cnstrcvs  25075  cncvs  25079  recvs  25080  qcvs  25081  zclmncvs  25082  tcphex  25151  cnfldcusp  25291  resscdrg  25292  reust  25315  recusp  25316  vitalilem4  25546  vitalilem5  25547  mbfdm  25561  dveflem  25917  dvlipcn  25933  c1lip2  25937  dgrid  26204  iaa  26267  abelthlem3  26377  abelthlem5  26379  abelth  26385  efcn  26387  sinhalfpilem  26406  sincosq1lem  26440  sincosq4sgn  26444  tangtx  26448  sincos4thpi  26456  sincos6thpi  26459  pigt3  26461  pige3ALT  26463  cos0pilt1  26475  logi  26530  relogcn  26581  dvlog2lem  26595  dvlog2  26596  logtayl  26603  logtayl2  26605  cxpsqrtlem  26645  cxpsqrt  26646  2irrexpq  26674  cxpcn2  26690  cxpcn3  26692  logblog  26736  2logb9irr  26739  2logb3irr  26741  2logb9irrALT  26742  sqrt2cxp2logb9e3  26743  2irrexpqALT  26744  ang180lem1  26753  ang180lem2  26754  1cubrlem  26785  mcubic  26791  quart1lem  26799  quart1  26800  reasinsin  26840  atancj  26854  efiatan  26856  atantan  26867  atanbndlem  26869  atan1  26872  atancn  26880  atantayl2  26882  log2cnv  26888  log2tlbnd  26889  log2ublem1  26890  log2ublem2  26891  log2ub  26893  efrlim  26913  efrlimOLD  26914  scvxcvx  26930  1sgm2ppw  27145  ppiub  27149  bclbnd  27225  bposlem8  27236  lgsdir2lem1  27270  lgsdir2lem5  27274  lgseisenlem1  27320  lgseisenlem2  27321  lgsquadlem1  27325  chebbnd1  27417  dchrvmasumlem2  27443  norecfn  27894  norec2fn  27904  addsproplem2  27918  addsproplem6  27922  addsbdaylem  27964  negs1s  27974  negsproplem2  27976  mulsproplem2  28061  mulsproplem3  28062  mulsproplem5  28064  mulsproplem6  28065  mulsproplem7  28066  mulsproplem8  28067  mulsproplem13  28072  mulsproplem14  28073  0zs  28317  zseo  28350  twocut  28351  istrkg3ld  28442  trgcgrg  28496  ax5seglem7  28916  axlowdimlem6  28928  axlowdimlem8  28930  axlowdimlem11  28933  elntg2  28966  cusgrsizeindb1  29432  vtxdginducedm1  29525  0grrusgr  29561  erclwwlktr  30002  erclwwlkntr  30051  wlk2v2e  30137  upgr3v3e3cycl  30160  konigsberglem1  30232  konigsberglem2  30233  konigsberglem3  30234  konigsberglem5  30236  ex-fl  30427  ex-mod  30429  ex-hash  30433  ex-lcm  30438  0vfval  30586  smcnlem  30677  lnocoi  30737  nmlno0lem  30773  nmblolbii  30779  blocnilem  30784  blocni  30785  cncph  30799  isph  30802  ip0i  30805  ip1ilem  30806  ip2i  30808  ipdirilem  30809  ipasslem7  30816  ipasslem8  30817  ipasslem9  30818  ipasslem10  30819  ipasslem11  30820  ip2dii  30824  pythi  30830  siilem1  30831  siilem2  30832  siii  30833  hvmulassi  31026  hvmulcomi  31027  hvdistr1i  31031  hvsubdistr1i  31032  hvassi  31033  hvadd32i  31034  hvsubassi  31035  hvsub32i  31036  normlem0  31089  normlem8  31097  normlem9  31098  bcseqi  31100  polid2i  31137  hhph  31158  hlim0  31215  shscli  31297  shlessi  31357  shlej1i  31358  omlsilem  31382  shlubi  31395  h1de2i  31533  pjadjii  31654  pjaddii  31655  pjmulii  31657  pjdifnormii  31663  pjcji  31664  hoaddsubassi  31800  eigrei  31814  eigposi  31816  eigorthi  31817  adj0  31974  lnopeq0lem1  31985  lnopunilem1  31990  lnophmlem2  31997  nmcexi  32006  nmcopexi  32007  lnfn0i  32022  nmcfnexi  32031  mdexchi  32315  xppreima2  32626  sgnclre  32808  dp2clq  32852  dp2lt  32856  dp2ltc  32858  dpexpp1  32879  dpmul  32884  dpmul4  32885  elxrge02  32903  xrge0adddir  33003  psgnid  33070  cnmsgn0g  33119  altgnsg  33122  xrnarchi  33154  xrge0slmod  33313  znfermltl  33331  ccfldextdgrr  33661  cos9thpiminplylem4  33769  cos9thpiminplylem5  33770  raddcn  33913  xrge0iifcnv  33917  xrge0iifiso  33919  xrge0iifhmeo  33920  xrge0iifhom  33921  xrge0iifmhm  33923  xrge0mulc1cn  33925  lmlimxrge0  33932  pnfneige0  33935  lmxrge0  33936  zringnm  33942  rezh  33953  qqh0  33968  qqh1  33969  qqhucn  33976  esumpinfval  34057  hashf2  34068  esumcvg  34070  br2base  34254  sxbrsigalem3  34257  dya2iocbrsiga  34260  dya2icobrsiga  34261  sxbrsigalem1  34270  sxbrsigalem2  34271  sxbrsigalem4  34272  sxbrsigalem5  34273  sxbrsiga  34275  ballotlem2  34474  ballotlem4  34484  ballotlemi1  34488  ballotth  34523  signstf  34551  itgexpif  34591  chtvalz  34614  hgt750lemd  34633  hgt750lem  34636  tgoldbachgnn  34644  lfuhgr2  35100  subfacp1lem1  35160  subfacp1lem6  35166  kur14lem6  35192  cvmliftlem4  35269  satf0suc  35357  problem4  35649  quad3  35651  iexpire  35716  fununiq  35750  fvtransport  36014  bj-minftyccb  37207  taupilem2  37304  iccioo01  37309  1oequni2o  37350  finxp1o  37374  finxpreclem4  37376  cos2h  37599  tan2h  37600  poimirlem9  37617  poimirlem27  37635  poimirlem28  37636  ismblfin  37649  mbfposadd  37655  ftc1anclem5  37685  asindmre  37691  dvasin  37692  dvacos  37693  rrnval  37815  dihjatcclem4  41409  lcmineqlem12  42022  fisdomnn  42226  subex  42229  absex  42230  cjex  42231  cxpi11d  42325  redvmptabs  42342  readvrec  42344  sn-00idlem2  42381  sn-00id  42383  remul02  42387  rabren3dioph  42797  jm2.27dlem2  42993  rmydioph  42997  rmxdioph  42999  expdiophlem2  43005  expdioph  43006  arearect  43198  areaquad  43199  2omomeqom  43286  omnord1ex  43287  corclrcl  43690  iunrelexpuztr  43702  corcltrcl  43722  dffrege76  43922  k0004val0  44137  lhe4.4ex1a  44312  binomcxplemdvbinom  44336  binomcxplemnotnn0  44339  ax6e2ndeqALT  44914  sineq0ALT  44920  nregmodelf1o  44999  pnfel0pnf  45520  lptioo2cn  45637  limsup10ex  45765  liminf10ex  45766  icccncfext  45879  itgsin0pilem1  45942  itgsbtaddcnst  45974  stoweidlem13  46005  wallispilem2  46058  wallispilem4  46060  wallispi2lem1  46063  stirlinglem13  46078  dirkerper  46088  dirkertrigeqlem3  46092  dirkeritg  46094  dirkercncflem1  46095  dirkercncflem4  46098  fourierdlem42  46141  fourierdlem62  46160  fourierdlem102  46200  fourierdlem103  46201  fourierdlem104  46202  fourierdlem114  46212  sqwvfoura  46220  fourierswlem  46222  fouriersw  46223  smfmullem4  46786  ceil5half3  47335  8mod5e3  47355  fmtnoprmfac2lem1  47561  fmtno4prm  47570  3exp4mod41  47611  41prothprmlem2  47613  6gbe  47766  7gbow  47767  8gbe  47768  9gbo  47769  11gbo  47770  sbgoldbalt  47776  nnsum4primesevenALTV  47796  usgrexmpl2nb0  48016  usgrexmpl2nb3  48019  gpg3nbgrvtx0  48061  gpg3nbgrvtx0ALT  48062  gpg3nbgrvtx1  48063  gpg5grlic  48078  0nodd  48152  oddinmgm  48157  2zrng0  48226  zlmodzxz0  48338  zlmodzxzequa  48479  zlmodzxzequap  48482  zlmodzxzldeplem3  48485  nnlog2ge0lt1  48549  blen1  48567  blen2  48568  nnolog2flm1  48573  ackval42  48679  ehl2eudisval0  48708  line2ylem  48734  i0oii  48902  io1ii  48903  sepfsepc  48910  rescofuf  49076  setc1ohomfval  49476  setc1ocofval  49477