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  4655  rextp  4656  opthhausdorff  5455  funopg  6515  feq12i  6644  ftp  7090  caovass  7546  caovdi  7565  ordom  7806  mptexw  7885  ofmres  7916  sbcoteq1a  7983  mpoexw  8010  xpord3lem  8079  omopthlem1  8574  omopthlem2  8575  omopthi  8576  on2recsfn  8582  xpcomen  8981  snnen2o  9129  unfilem3  9191  hartogs  9430  card2on  9440  unwf  9703  inlresf1  9808  inrresf1  9810  tskwe  9843  alephsmo  9993  dfac4  10013  dfac2a  10021  ackbij1lem13  10122  axdc2lem  10339  axcclem  10348  ondomon  10454  cfpwsdom  10475  pwfseqlem2  10550  pwfseqlem3  10551  1lt2pi  10796  addassi  11122  mulassi  11123  adddii  11124  adddiri  11125  lttri  11239  lelttri  11240  ltletri  11241  letri  11242  ltadd2i  11244  mul02lem2  11290  addrid  11293  addcani  11306  addcan2i  11307  mul12i  11308  mul32i  11309  add12i  11336  add32i  11337  subaddi  11448  subadd2i  11449  subsub23i  11451  addsubassi  11452  addsubi  11453  subcani  11454  subcan2i  11455  pnncani  11456  subdii  11566  subdiri  11567  ltadd1i  11671  leadd1i  11672  leadd2i  11673  ltsubaddi  11674  lesubaddi  11675  ltsubadd2i  11676  lesubadd2i  11677  ltaddsubi  11678  mulcani  11756  div23i  11879  div11i  11880  3halfnz  12552  mpoaddex  12886  addex  12887  mpomulex  12888  mulex  12889  unirnioo  13349  ioorebas  13351  xnn0xrge0  13406  fldiv4lem1div2  13741  uzenom  13871  nnenom  13887  seqexw  13924  m1expcl2  13992  i4  14111  expnass  14115  faclbnd4lem1  14200  bcn1  14220  hashfxnn0  14244  ccat2s1p1  14537  ccat2s1p2  14538  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  ex-chn2  18544  0symgefmndeq  19306  pmtrprfval  19399  m1expaddsub  19410  0frgp  19691  staffval  20756  cnfldcj  21300  cnfldds  21303  cnfldfunALT  21306  cnfldcjOLD  21313  cnflddsOLD  21316  cnfldfunALTOLD  21319  xrsadd  21322  xrsmul  21323  xrsds  21346  cnmgpid  21366  nn0srg  21374  rge0srg  21375  zring0  21395  pzriprnglem13  21430  pzriprng1ALT  21433  fermltlchr  21466  cnmsgnsubg  21514  psgninv  21519  re0g  21549  ocvfval  21603  frlmbas  21692  mdetrlin  22517  mdetunilem9  22535  leordtval2  23127  iscnp2  23154  utop3cls  24166  nmfval  24503  nmoffn  24626  nmofval  24629  icccld  24681  addcnlem  24780  iimulcn  24861  iimulcnOLD  24862  icopnfhmeo  24868  iccpnfcnv  24869  iccpnfhmeo  24870  xrhmeo  24871  xrhmph  24872  oprpiece1res1  24876  oprpiece1res2  24877  ishtpy  24898  pcoass  24951  cnstrcvs  25068  cncvs  25072  recvs  25073  qcvs  25074  zclmncvs  25075  tcphex  25144  cnfldcusp  25284  resscdrg  25285  reust  25308  recusp  25309  vitalilem4  25539  vitalilem5  25540  mbfdm  25554  dveflem  25910  dvlipcn  25926  c1lip2  25930  dgrid  26197  iaa  26260  abelthlem3  26370  abelthlem5  26372  abelth  26378  efcn  26380  sinhalfpilem  26399  sincosq1lem  26433  sincosq4sgn  26437  tangtx  26441  sincos4thpi  26449  sincos6thpi  26452  pigt3  26454  pige3ALT  26456  cos0pilt1  26468  logi  26523  relogcn  26574  dvlog2lem  26588  dvlog2  26589  logtayl  26596  logtayl2  26598  cxpsqrtlem  26638  cxpsqrt  26639  2irrexpq  26667  cxpcn2  26683  cxpcn3  26685  logblog  26729  2logb9irr  26732  2logb3irr  26734  2logb9irrALT  26735  sqrt2cxp2logb9e3  26736  2irrexpqALT  26737  ang180lem1  26746  ang180lem2  26747  1cubrlem  26778  mcubic  26784  quart1lem  26792  quart1  26793  reasinsin  26833  atancj  26847  efiatan  26849  atantan  26860  atanbndlem  26862  atan1  26865  atancn  26873  atantayl2  26875  log2cnv  26881  log2tlbnd  26882  log2ublem1  26883  log2ublem2  26884  log2ub  26886  efrlim  26906  efrlimOLD  26907  scvxcvx  26923  1sgm2ppw  27138  ppiub  27142  bclbnd  27218  bposlem8  27229  lgsdir2lem1  27263  lgsdir2lem5  27267  lgseisenlem1  27313  lgseisenlem2  27314  lgsquadlem1  27318  chebbnd1  27410  dchrvmasumlem2  27436  norecfn  27889  norec2fn  27899  addsproplem2  27913  addsproplem6  27917  addsbdaylem  27959  negs1s  27969  negsproplem2  27971  mulsproplem2  28056  mulsproplem3  28057  mulsproplem5  28059  mulsproplem6  28060  mulsproplem7  28061  mulsproplem8  28062  mulsproplem13  28067  mulsproplem14  28068  0zs  28312  zseo  28345  twocut  28346  istrkg3ld  28439  trgcgrg  28493  ax5seglem7  28913  axlowdimlem6  28925  axlowdimlem8  28927  axlowdimlem11  28930  elntg2  28963  cusgrsizeindb1  29429  vtxdginducedm1  29522  0grrusgr  29558  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  32633  sgnclre  32815  dp2clq  32861  dp2lt  32865  dp2ltc  32867  dpexpp1  32888  dpmul  32893  dpmul4  32894  elxrge02  32912  xrge0adddir  32999  psgnid  33066  cnmsgn0g  33115  altgnsg  33118  xrnarchi  33153  xrge0slmod  33313  znfermltl  33331  ccfldextdgrr  33685  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  raddcn  33942  xrge0iifcnv  33946  xrge0iifiso  33948  xrge0iifhmeo  33949  xrge0iifhom  33950  xrge0iifmhm  33952  xrge0mulc1cn  33954  lmlimxrge0  33961  pnfneige0  33964  lmxrge0  33965  zringnm  33971  rezh  33982  qqh0  33997  qqh1  33998  qqhucn  34005  esumpinfval  34086  hashf2  34097  esumcvg  34099  br2base  34282  sxbrsigalem3  34285  dya2iocbrsiga  34288  dya2icobrsiga  34289  sxbrsigalem1  34298  sxbrsigalem2  34299  sxbrsigalem4  34300  sxbrsigalem5  34301  sxbrsiga  34303  ballotlem2  34502  ballotlem4  34512  ballotlemi1  34516  ballotth  34551  signstf  34579  itgexpif  34619  chtvalz  34642  hgt750lemd  34661  hgt750lem  34664  tgoldbachgnn  34672  lfuhgr2  35163  subfacp1lem1  35223  subfacp1lem6  35229  kur14lem6  35255  cvmliftlem4  35332  satf0suc  35420  problem4  35712  quad3  35714  iexpire  35779  fununiq  35813  fvtransport  36076  bj-minftyccb  37269  taupilem2  37366  iccioo01  37371  1oequni2o  37412  finxp1o  37436  finxpreclem4  37438  cos2h  37650  tan2h  37651  poimirlem9  37668  poimirlem27  37686  poimirlem28  37687  ismblfin  37700  mbfposadd  37706  ftc1anclem5  37736  asindmre  37742  dvasin  37743  dvacos  37744  rrnval  37866  dihjatcclem4  41519  lcmineqlem12  42132  fisdomnn  42336  subex  42339  absex  42340  cjex  42341  cxpi11d  42435  redvmptabs  42452  readvrec  42454  sn-00idlem2  42491  sn-00id  42493  remul02  42497  rabren3dioph  42907  jm2.27dlem2  43102  rmydioph  43106  rmxdioph  43108  expdiophlem2  43114  expdioph  43115  arearect  43307  areaquad  43308  2omomeqom  43395  omnord1ex  43396  corclrcl  43799  iunrelexpuztr  43811  corcltrcl  43831  dffrege76  44031  k0004val0  44246  lhe4.4ex1a  44421  binomcxplemdvbinom  44445  binomcxplemnotnn0  44448  ax6e2ndeqALT  45022  sineq0ALT  45028  nregmodelf1o  45107  pnfel0pnf  45627  lptioo2cn  45742  limsup10ex  45870  liminf10ex  45871  icccncfext  45984  itgsin0pilem1  46047  itgsbtaddcnst  46079  stoweidlem13  46110  wallispilem2  46163  wallispilem4  46165  wallispi2lem1  46168  stirlinglem13  46183  dirkerper  46193  dirkertrigeqlem3  46197  dirkeritg  46199  dirkercncflem1  46200  dirkercncflem4  46203  fourierdlem42  46246  fourierdlem62  46265  fourierdlem102  46305  fourierdlem103  46306  fourierdlem104  46307  fourierdlem114  46317  sqwvfoura  46325  fourierswlem  46327  fouriersw  46328  smfmullem4  46891  nthrucw  46983  ceil5half3  47439  8mod5e3  47459  fmtnoprmfac2lem1  47665  fmtno4prm  47674  3exp4mod41  47715  41prothprmlem2  47717  6gbe  47870  7gbow  47871  8gbe  47872  9gbo  47873  11gbo  47874  sbgoldbalt  47880  nnsum4primesevenALTV  47900  usgrexmpl2nb0  48130  usgrexmpl2nb3  48133  gpg3nbgrvtx0  48175  gpg3nbgrvtx0ALT  48176  gpg3nbgrvtx1  48177  gpg5grlim  48192  gpg5grlic  48193  0nodd  48269  oddinmgm  48274  2zrng0  48343  zlmodzxz0  48455  zlmodzxzequa  48596  zlmodzxzequap  48599  zlmodzxzldeplem3  48602  nnlog2ge0lt1  48666  blen1  48684  blen2  48685  nnolog2flm1  48690  ackval42  48796  ehl2eudisval0  48825  line2ylem  48851  i0oii  49019  io1ii  49020  sepfsepc  49027  rescofuf  49193  setc1ohomfval  49593  setc1ocofval  49594