Theorem mp3an 1461

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  el3v  3496  raltp  4730  rextp  4731  opthhausdorff  5536  funopg  6612  feq12i  6740  ftp  7191  caovass  7650  caovdi  7669  ordom  7913  mptexw  7993  ofmres  8025  sbcoteq1a  8092  mpoexw  8119  xpord3lem  8190  omopthlem1  8715  omopthlem2  8716  omopthi  8717  on2recsfn  8723  xpcomen  9129  snnen2o  9300  unfilem3  9373  hartogs  9613  card2on  9623  unwf  9879  inlresf1  9984  inrresf1  9986  tskwe  10019  alephsmo  10171  dfac4  10191  dfac2a  10199  ackbij1lem13  10300  axdc2lem  10517  axcclem  10526  ondomon  10632  cfpwsdom  10653  pwfseqlem2  10728  pwfseqlem3  10729  1lt2pi  10974  addassi  11300  mulassi  11301  adddii  11302  adddiri  11303  lttri  11416  lelttri  11417  ltletri  11418  letri  11419  ltadd2i  11421  mul02lem2  11467  addrid  11470  addcani  11483  addcan2i  11484  mul12i  11485  mul32i  11486  add12i  11512  add32i  11513  subaddi  11623  subadd2i  11624  subsub23i  11626  addsubassi  11627  addsubi  11628  subcani  11629  subcan2i  11630  pnncani  11631  subdii  11739  subdiri  11740  ltadd1i  11844  leadd1i  11845  leadd2i  11846  ltsubaddi  11847  lesubaddi  11848  ltsubadd2i  11849  lesubadd2i  11850  ltaddsubi  11851  mulcani  11929  div23i  12052  div11i  12053  1mhlfehlf  12512  halfpm6th  12514  3halfnz  12722  mpoaddex  13053  addex  13054  mpomulex  13055  mulex  13056  unirnioo  13509  ioorebas  13511  xnn0xrge0  13566  fldiv4lem1div2  13888  uzenom  14015  nnenom  14031  seqexw  14068  m1expcl2  14136  i4  14253  expnass  14257  faclbnd4lem1  14342  bcn1  14362  hashfxnn0  14386  ccat2s1p1  14677  ccat2s1p2  14678  cats1fvn  14907  cats1fv  14908  cats1cat  14910  cats2cat  14911  wrdlen3s3  14998  abs3difi  15458  0.999...  15929  bpoly3  16106  ef01bndlem  16232  cos1bnd  16235  cos2bnd  16236  sin4lt0  16243  rpnnen2lem3  16264  rpnnen2lem11  16272  rpnnen  16275  rexpen  16276  aleph1irr  16294  3dvdsdec  16380  3dvds2dec  16381  divalglem2  16443  ndvdsi  16460  flodddiv4  16461  gcdaddmlem  16570  bezout  16590  3lcm2e6woprm  16662  6lcm4e12  16663  lcmf0  16681  lcmf2a3a4e12  16694  dec2dvds  17110  modxai  17115  modsubi  17119  gcdi  17120  numexp2x  17126  2exp5  17133  2exp11  17137  0symgefmndeq  19435  pmtrprfval  19529  m1expaddsub  19540  0frgp  19821  staffval  20864  cnfldcj  21396  cnfldds  21399  cnfldfunALT  21402  cnfldcjOLD  21409  cnflddsOLD  21412  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  xrsadd  21420  xrsmul  21421  xrsds  21450  cnmgpid  21470  nn0srg  21478  rge0srg  21479  zring0  21492  pzriprnglem13  21527  pzriprng1ALT  21530  fermltlchr  21567  cnmsgnsubg  21618  psgninv  21623  re0g  21653  ocvfval  21707  frlmbas  21798  mdetrlin  22629  mdetunilem9  22647  leordtval2  23241  iscnp2  23268  utop3cls  24281  nmfval  24622  nmoffn  24753  nmofval  24756  icccld  24808  addcnlem  24905  iimulcn  24986  iimulcnOLD  24987  icopnfhmeo  24993  iccpnfcnv  24994  iccpnfhmeo  24995  xrhmeo  24996  xrhmph  24997  oprpiece1res1  25001  oprpiece1res2  25002  ishtpy  25023  pcoass  25076  cnstrcvs  25193  cncvs  25197  recvs  25198  recvsOLD  25199  qcvs  25200  zclmncvs  25201  tcphex  25270  cnfldcusp  25410  resscdrg  25411  reust  25434  recusp  25435  vitalilem4  25665  vitalilem5  25666  mbfdm  25680  dveflem  26037  dvlipcn  26053  c1lip2  26057  dgrid  26324  iaa  26385  abelthlem3  26495  abelthlem5  26497  abelth  26503  efcn  26505  sinhalfpilem  26523  sincosq1lem  26557  sincosq4sgn  26561  tangtx  26565  sincos4thpi  26573  sincos6thpi  26576  pigt3  26578  pige3ALT  26580  cos0pilt1  26592  logi  26647  relogcn  26698  dvlog2lem  26712  dvlog2  26713  logtayl  26720  logtayl2  26722  cxpsqrtlem  26762  cxpsqrt  26763  2irrexpq  26791  cxpcn2  26807  cxpcn3  26809  logblog  26853  2logb9irr  26856  2logb3irr  26858  2logb9irrALT  26859  sqrt2cxp2logb9e3  26860  2irrexpqALT  26861  ang180lem1  26870  ang180lem2  26871  1cubrlem  26902  mcubic  26908  quart1lem  26916  quart1  26917  reasinsin  26957  atancj  26971  efiatan  26973  atantan  26984  atanbndlem  26986  atan1  26989  atancn  26997  atantayl2  26999  log2cnv  27005  log2tlbnd  27006  log2ublem1  27007  log2ublem2  27008  log2ub  27010  efrlim  27030  efrlimOLD  27031  scvxcvx  27047  1sgm2ppw  27262  ppiub  27266  bclbnd  27342  bposlem8  27353  lgsdir2lem1  27387  lgsdir2lem5  27391  lgseisenlem1  27437  lgseisenlem2  27438  lgsquadlem1  27442  chebbnd1  27534  dchrvmasumlem2  27560  norecfn  27997  norec2fn  28007  addsproplem2  28021  addsproplem6  28025  addsbdaylem  28067  negs1s  28077  negsproplem2  28079  mulsproplem2  28161  mulsproplem3  28162  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  mulsproplem13  28172  mulsproplem14  28173  0zs  28392  zseo  28424  nohalf  28425  istrkg3ld  28487  trgcgrg  28541  ax5seglem7  28968  axlowdimlem6  28980  axlowdimlem8  28982  axlowdimlem11  28985  elntg2  29018  cusgrsizeindb1  29486  vtxdginducedm1  29579  0grrusgr  29615  erclwwlktr  30054  erclwwlkntr  30103  wlk2v2e  30189  upgr3v3e3cycl  30212  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  konigsberglem5  30288  ex-fl  30479  ex-mod  30481  ex-hash  30485  ex-lcm  30490  0vfval  30638  smcnlem  30729  lnocoi  30789  nmlno0lem  30825  nmblolbii  30831  blocnilem  30836  blocni  30837  cncph  30851  isph  30854  ip0i  30857  ip1ilem  30858  ip2i  30860  ipdirilem  30861  ipasslem7  30868  ipasslem8  30869  ipasslem9  30870  ipasslem10  30871  ipasslem11  30872  ip2dii  30876  pythi  30882  siilem1  30883  siilem2  30884  siii  30885  hvmulassi  31078  hvmulcomi  31079  hvdistr1i  31083  hvsubdistr1i  31084  hvassi  31085  hvadd32i  31086  hvsubassi  31087  hvsub32i  31088  normlem0  31141  normlem8  31149  normlem9  31150  bcseqi  31152  polid2i  31189  hhph  31210  hlim0  31267  shscli  31349  shlessi  31409  shlej1i  31410  omlsilem  31434  shlubi  31447  h1de2i  31585  pjadjii  31706  pjaddii  31707  pjmulii  31709  pjdifnormii  31715  pjcji  31716  hoaddsubassi  31852  eigrei  31866  eigposi  31868  eigorthi  31869  adj0  32026  lnopeq0lem1  32037  lnopunilem1  32042  lnophmlem2  32049  nmcexi  32058  nmcopexi  32059  lnfn0i  32074  nmcfnexi  32083  mdexchi  32367  xppreima2  32669  dp2clq  32845  dp2lt  32849  dp2ltc  32851  dpexpp1  32872  dpmul  32877  dpmul4  32878  elxrge02  32896  xrge0adddir  33004  psgnid  33090  cnmsgn0g  33139  altgnsg  33142  xrnarchi  33164  xrge0slmod  33341  znfermltl  33359  ccfldextdgrr  33682  raddcn  33875  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhmeo  33882  xrge0iifhom  33883  xrge0iifmhm  33885  xrge0mulc1cn  33887  lmlimxrge0  33894  pnfneige0  33897  lmxrge0  33898  zringnm  33904  rezh  33917  qqh0  33930  qqh1  33931  qqhucn  33938  esumpinfval  34037  hashf2  34048  esumcvg  34050  br2base  34234  sxbrsigalem3  34237  dya2iocbrsiga  34240  dya2icobrsiga  34241  sxbrsigalem1  34250  sxbrsigalem2  34251  sxbrsigalem4  34252  sxbrsigalem5  34253  sxbrsiga  34255  ballotlem2  34453  ballotlem4  34463  ballotlemi1  34467  ballotth  34502  sgnclre  34504  signstf  34543  itgexpif  34583  chtvalz  34606  hgt750lemd  34625  hgt750lem  34628  tgoldbachgnn  34636  lfuhgr2  35086  subfacp1lem1  35147  subfacp1lem6  35153  kur14lem6  35179  cvmliftlem4  35256  satf0suc  35344  problem4  35636  quad3  35638  iexpire  35697  fununiq  35732  fvtransport  35996  bj-minftyccb  37191  taupilem2  37288  iccioo01  37293  1oequni2o  37334  finxp1o  37358  finxpreclem4  37360  cos2h  37571  tan2h  37572  poimirlem9  37589  poimirlem27  37607  poimirlem28  37608  ismblfin  37621  mbfposadd  37627  ftc1anclem5  37657  asindmre  37663  dvasin  37664  dvacos  37665  rrnval  37787  dihjatcclem4  41378  lcmineqlem12  41997  fisdomnn  42239  subex  42242  absex  42243  cjex  42244  cxpi11d  42331  sn-00idlem2  42375  sn-00id  42377  remul02  42381  rabren3dioph  42771  jm2.27dlem2  42967  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  arearect  43176  areaquad  43177  2omomeqom  43265  omnord1ex  43266  corclrcl  43669  iunrelexpuztr  43681  corcltrcl  43701  dffrege76  43901  k0004val0  44116  lhe4.4ex1a  44298  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  ax6e2ndeqALT  44902  sineq0ALT  44908  pnfel0pnf  45446  lptioo2cn  45566  limsup10ex  45694  liminf10ex  45695  icccncfext  45808  itgsin0pilem1  45871  itgsbtaddcnst  45903  stoweidlem13  45934  wallispilem2  45987  wallispilem4  45989  wallispi2lem1  45992  stirlinglem13  46007  dirkerper  46017  dirkertrigeqlem3  46021  dirkeritg  46023  dirkercncflem1  46024  dirkercncflem4  46027  fourierdlem42  46070  fourierdlem62  46089  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  sqwvfoura  46149  fourierswlem  46151  fouriersw  46152  smfmullem4  46715  fmtnoprmfac2lem1  47440  fmtno4prm  47449  3exp4mod41  47490  41prothprmlem2  47492  6gbe  47645  7gbow  47646  8gbe  47647  9gbo  47648  11gbo  47649  sbgoldbalt  47655  nnsum4primesevenALTV  47675  usgrexmpl2nb0  47846  usgrexmpl2nb3  47849  0nodd  47893  oddinmgm  47898  2zrng0  47967  zlmodzxz0  48081  zlmodzxzequa  48225  zlmodzxzequap  48228  zlmodzxzldeplem3  48231  nnlog2ge0lt1  48300  blen1  48318  blen2  48319  nnolog2flm1  48324  ackval42  48430  ehl2eudisval0  48459  line2ylem  48485  i0oii  48599  io1ii  48600  sepfsepc  48607