Theorem mp3an 1464

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 1451	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 693	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  3435  raltp  4639  rextp  4640  opthhausdorff  5460  funopg  6521  feq12i  6650  ftp  7100  caovass  7556  caovdi  7575  ordom  7816  mptexw  7895  ofmres  7926  sbcoteq1a  7993  mpoexw  8020  xpord3lem  8088  omopthlem1  8584  omopthlem2  8585  omopthi  8586  on2recsfn  8592  xpcomen  8995  snnen2o  9144  unfilem3  9206  hartogs  9448  card2on  9458  unwf  9723  inlresf1  9828  inrresf1  9830  tskwe  9863  alephsmo  10013  dfac4  10033  dfac2a  10041  ackbij1lem13  10142  axdc2lem  10359  axcclem  10368  ondomon  10474  cfpwsdom  10496  pwfseqlem2  10571  pwfseqlem3  10572  1lt2pi  10817  addassi  11144  mulassi  11145  adddii  11146  adddiri  11147  lttri  11261  lelttri  11262  ltletri  11263  letri  11264  ltadd2i  11266  mul02lem2  11312  addrid  11315  addcani  11328  addcan2i  11329  mul12i  11330  mul32i  11331  add12i  11358  add32i  11359  subaddi  11470  subadd2i  11471  subsub23i  11473  addsubassi  11474  addsubi  11475  subcani  11476  subcan2i  11477  pnncani  11478  subdii  11588  subdiri  11589  ltadd1i  11693  leadd1i  11694  leadd2i  11695  ltsubaddi  11696  lesubaddi  11697  ltsubadd2i  11698  lesubadd2i  11699  ltaddsubi  11700  mulcani  11778  div23i  11902  div11i  11903  3halfnz  12597  mpoaddex  12927  addex  12928  mpomulex  12929  mulex  12930  unirnioo  13391  ioorebas  13393  xnn0xrge0  13448  fldiv4lem1div2  13785  uzenom  13915  nnenom  13931  seqexw  13968  m1expcl2  14036  i4  14155  expnass  14159  faclbnd4lem1  14244  bcn1  14264  hashfxnn0  14288  ccat2s1p1  14581  ccat2s1p2  14582  cats1fvn  14809  cats1fv  14810  cats1cat  14812  cats2cat  14813  wrdlen3s3  14900  abs3difi  15361  0.999...  15835  bpoly3  16012  ef01bndlem  16140  cos1bnd  16143  cos2bnd  16144  sin4lt0  16151  rpnnen2lem3  16172  rpnnen2lem11  16180  rpnnen  16183  rexpen  16184  aleph1irr  16202  3dvdsdec  16290  3dvds2dec  16291  divalglem2  16353  ndvdsi  16370  flodddiv4  16373  gcdaddmlem  16482  bezout  16501  3lcm2e6woprm  16573  6lcm4e12  16574  lcmf0  16592  lcmf2a3a4e12  16605  dec2dvds  17023  modxai  17028  modsubi  17032  gcdi  17033  numexp2x  17038  2exp5  17045  2exp11  17049  ex-chn2  18593  0symgefmndeq  19358  pmtrprfval  19451  m1expaddsub  19462  0frgp  19743  staffval  20807  cnfldcj  21350  cnfldds  21353  cnfldfunALT  21356  xrsadd  21359  xrsmul  21360  xrsds  21379  cnmgpid  21398  nn0srg  21406  rge0srg  21407  zring0  21427  pzriprnglem13  21462  pzriprng1ALT  21465  fermltlchr  21498  cnmsgnsubg  21546  psgninv  21551  re0g  21581  ocvfval  21635  frlmbas  21724  mdetrlin  22555  mdetunilem9  22573  leordtval2  23165  iscnp2  23192  utop3cls  24204  nmfval  24541  nmoffn  24664  nmofval  24667  icccld  24719  addcnlem  24818  iimulcn  24893  icopnfhmeo  24898  iccpnfcnv  24899  iccpnfhmeo  24900  xrhmeo  24901  xrhmph  24902  oprpiece1res1  24906  oprpiece1res2  24907  ishtpy  24927  pcoass  24979  cnstrcvs  25096  cncvs  25100  recvs  25101  qcvs  25102  zclmncvs  25103  tcphex  25172  cnfldcusp  25312  resscdrg  25313  reust  25336  recusp  25337  vitalilem4  25566  vitalilem5  25567  mbfdm  25581  dveflem  25934  dvlipcn  25949  c1lip2  25953  dgrid  26217  iaa  26279  abelthlem3  26386  abelthlem5  26388  abelth  26394  efcn  26396  sinhalfpilem  26415  sincosq1lem  26449  sincosq4sgn  26453  tangtx  26457  sincos4thpi  26465  sincos6thpi  26468  pigt3  26470  pige3ALT  26472  cos0pilt1  26484  logi  26539  relogcn  26590  dvlog2lem  26604  dvlog2  26605  logtayl  26612  logtayl2  26614  cxpsqrtlem  26654  cxpsqrt  26655  2irrexpq  26683  cxpcn2  26698  cxpcn3  26700  logblog  26744  2logb9irr  26747  2logb3irr  26749  2logb9irrALT  26750  sqrt2cxp2logb9e3  26751  2irrexpqALT  26752  ang180lem1  26761  ang180lem2  26762  1cubrlem  26793  mcubic  26799  quart1lem  26807  quart1  26808  reasinsin  26848  atancj  26862  efiatan  26864  atantan  26875  atanbndlem  26877  atan1  26880  atancn  26888  atantayl2  26890  log2cnv  26896  log2tlbnd  26897  log2ublem1  26898  log2ublem2  26899  log2ub  26901  efrlim  26921  scvxcvx  26937  1sgm2ppw  27151  ppiub  27155  bclbnd  27231  bposlem8  27242  lgsdir2lem1  27276  lgsdir2lem5  27280  lgseisenlem1  27326  lgseisenlem2  27327  lgsquadlem1  27331  chebbnd1  27423  dchrvmasumlem2  27449  norecfn  27926  norec2fn  27936  addsproplem2  27950  addsproplem6  27954  addbdaylem  27997  neg1s  28007  negsproplem2  28009  mulsproplem2  28097  mulsproplem3  28098  mulsproplem5  28100  mulsproplem6  28101  mulsproplem7  28102  mulsproplem8  28103  mulsproplem13  28108  mulsproplem14  28109  0zs  28368  zseo  28402  twocut  28403  bdaypw2n0bndlem  28443  bdaypw2bnd  28445  bdayfinbndlem1  28447  z12bdaylem2  28451  istrkg3ld  28517  trgcgrg  28571  ax5seglem7  28992  axlowdimlem6  29004  axlowdimlem8  29006  axlowdimlem11  29009  elntg2  29042  cusgrsizeindb1  29507  vtxdginducedm1  29600  0grrusgr  29636  erclwwlktr  30080  erclwwlkntr  30129  wlk2v2e  30215  upgr3v3e3cycl  30238  konigsberglem1  30310  konigsberglem2  30311  konigsberglem3  30312  konigsberglem5  30314  ex-fl  30505  ex-mod  30507  ex-hash  30511  ex-lcm  30516  0vfval  30665  smcnlem  30756  lnocoi  30816  nmlno0lem  30852  nmblolbii  30858  blocnilem  30863  blocni  30864  cncph  30878  isph  30881  ip0i  30884  ip1ilem  30885  ip2i  30887  ipdirilem  30888  ipasslem7  30895  ipasslem8  30896  ipasslem9  30897  ipasslem10  30898  ipasslem11  30899  ip2dii  30903  pythi  30909  siilem1  30910  siilem2  30911  siii  30912  hvmulassi  31105  hvmulcomi  31106  hvdistr1i  31110  hvsubdistr1i  31111  hvassi  31112  hvadd32i  31113  hvsubassi  31114  hvsub32i  31115  normlem0  31168  normlem8  31176  normlem9  31177  bcseqi  31179  polid2i  31216  hhph  31237  hlim0  31294  shscli  31376  shlessi  31436  shlej1i  31437  omlsilem  31461  shlubi  31474  h1de2i  31612  pjadjii  31733  pjaddii  31734  pjmulii  31736  pjdifnormii  31742  pjcji  31743  hoaddsubassi  31879  eigrei  31893  eigposi  31895  eigorthi  31896  adj0  32053  lnopeq0lem1  32064  lnopunilem1  32069  lnophmlem2  32076  nmcexi  32085  nmcopexi  32086  lnfn0i  32101  nmcfnexi  32110  mdexchi  32394  xppreima2  32712  sgnclre  32893  dp2clq  32928  dp2lt  32932  dp2ltc  32934  dpexpp1  32955  dpmul  32960  dpmul4  32961  elxrge02  32979  xrge0adddir  33066  psgnid  33146  cnmsgn0g  33195  altgnsg  33198  xrnarchi  33233  xrge0slmod  33396  znfermltl  33414  ccfldextdgrr  33804  cos9thpiminplylem4  33917  cos9thpiminplylem5  33918  raddcn  34061  xrge0iifcnv  34065  xrge0iifiso  34067  xrge0iifhmeo  34068  xrge0iifhom  34069  xrge0iifmhm  34071  xrge0mulc1cn  34073  lmlimxrge0  34080  pnfneige0  34083  lmxrge0  34084  zringnm  34090  rezh  34101  qqh0  34116  qqh1  34117  qqhucn  34124  esumpinfval  34205  hashf2  34216  esumcvg  34218  br2base  34401  sxbrsigalem3  34404  dya2iocbrsiga  34407  dya2icobrsiga  34408  sxbrsigalem1  34417  sxbrsigalem2  34418  sxbrsigalem4  34419  sxbrsigalem5  34420  sxbrsiga  34422  ballotlem2  34621  ballotlem4  34631  ballotlemi1  34635  ballotth  34670  signstf  34698  itgexpif  34738  chtvalz  34761  hgt750lemd  34780  hgt750lem  34783  tgoldbachgnn  34791  lfuhgr2  35289  subfacp1lem1  35349  subfacp1lem6  35355  kur14lem6  35381  cvmliftlem4  35458  satf0suc  35546  problem4  35838  quad3  35840  iexpire  35905  fununiq  35939  fvtransport  36202  ttcid  36662  dfttc2g  36676  bj-minftyccb  37527  taupilem2  37624  iccioo01  37631  1oequni2o  37672  finxp1o  37696  finxpreclem4  37698  cos2h  37920  tan2h  37921  poimirlem9  37938  poimirlem27  37956  poimirlem28  37957  ismblfin  37970  mbfposadd  37976  ftc1anclem5  38006  asindmre  38012  dvasin  38013  dvacos  38014  rrnval  38136  dihjatcclem4  41855  lcmineqlem12  42467  fisdomnn  42671  subex  42674  absex  42675  cjex  42676  cxpi11d  42763  redvmptabs  42780  readvrec  42782  sn-00idlem2  42819  sn-00id  42821  remul02  42825  rabren3dioph  43231  jm2.27dlem2  43426  rmydioph  43430  rmxdioph  43432  expdiophlem2  43438  expdioph  43439  arearect  43631  areaquad  43632  2omomeqom  43719  omnord1ex  43720  corclrcl  44122  iunrelexpuztr  44134  corcltrcl  44154  dffrege76  44354  k0004val0  44569  lhe4.4ex1a  44744  binomcxplemdvbinom  44768  binomcxplemnotnn0  44771  ax6e2ndeqALT  45345  sineq0ALT  45351  nregmodelf1o  45430  pnfel0pnf  45946  lptioo2cn  46061  limsup10ex  46189  liminf10ex  46190  icccncfext  46303  itgsin0pilem1  46366  itgsbtaddcnst  46398  stoweidlem13  46429  wallispilem2  46482  wallispilem4  46484  wallispi2lem1  46487  stirlinglem13  46502  dirkerper  46512  dirkertrigeqlem3  46516  dirkeritg  46518  dirkercncflem1  46519  dirkercncflem4  46522  fourierdlem42  46565  fourierdlem62  46584  fourierdlem102  46624  fourierdlem103  46625  fourierdlem104  46626  fourierdlem114  46636  sqwvfoura  46644  fourierswlem  46646  fouriersw  46647  smfmullem4  47210  nthrucw  47304  goldracos5teq  47321  goldratmolem2  47322  ceil5half3  47782  8mod5e3  47802  fmtnoprmfac2lem1  48017  fmtno4prm  48026  3exp4mod41  48067  41prothprmlem2  48069  ppivalnn4  48078  6gbe  48235  7gbow  48236  8gbe  48237  9gbo  48238  11gbo  48239  sbgoldbalt  48245  nnsum4primesevenALTV  48265  usgrexmpl2nb0  48495  usgrexmpl2nb3  48498  gpg3nbgrvtx0  48540  gpg3nbgrvtx0ALT  48541  gpg3nbgrvtx1  48542  gpg5grlim  48557  gpg5grlic  48558  0nodd  48634  oddinmgm  48639  2zrng0  48708  zlmodzxz0  48820  zlmodzxzequa  48960  zlmodzxzequap  48963  zlmodzxzldeplem3  48966  nnlog2ge0lt1  49030  blen1  49048  blen2  49049  nnolog2flm1  49054  ackval42  49160  ehl2eudisval0  49189  line2ylem  49215  i0oii  49383  io1ii  49384  sepfsepc  49391  rescofuf  49556  setc1ohomfval  49956  setc1ocofval  49957