Theorem mp3an 1488

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  el3v  3461  raltp  4670  rextp  4671  opthhausdorff  5500  funopg  6570  feq12i  6698  ftp  7154  caovass  7610  caovdi  7629  ordom  7871  mptexw  7949  ofmres  7980  sbcoteq1a  8047  mpoexw  8074  xpord3lem  8144  omopthlem1  8644  omopthlem2  8645  omopthi  8646  on2recsfn  8652  xpcomen  9055  snnen2o  9204  unfilem3  9266  hartogs  9505  card2on  9515  unwf  9781  inlresf1  9900  inrresf1  9902  tskwe  9935  alephsmo  10085  dfac4  10105  dfac2a  10112  ackbij1lem13  10213  axdc2lem  10431  axcclem  10440  ondomon  10546  cfpwsdom  10568  pwfseqlem2  10643  pwfseqlem3  10644  1lt2pi  10889  addassi  11218  mulassi  11219  adddii  11220  adddiri  11221  lttri  11335  lelttri  11336  ltletri  11337  letri  11338  ltadd2i  11340  mul02lem2  11386  addrid  11389  addcani  11402  addcan2i  11403  mul12i  11404  mul32i  11405  add12i  11432  add32i  11433  subaddi  11544  subadd2i  11545  subsub23i  11547  addsubassi  11548  addsubi  11549  subcani  11550  subcan2i  11551  pnncani  11552  subdii  11662  subdiri  11663  ltadd1i  11767  leadd1i  11768  leadd2i  11769  ltsubaddi  11770  lesubaddi  11771  ltsubadd2i  11772  lesubadd2i  11773  ltaddsubi  11774  mulcani  11852  div23i  11972  div11i  11973  3halfnz  12674  mpoaddex  13011  addex  13012  mpomulex  13013  mulex  13014  unirnioo  13475  ioorebas  13477  xnn0xrge0  13532  fldiv4lem1div2  13869  uzenom  13999  nnenom  14015  seqexw  14052  m1expcl2  14120  i4  14239  expnass  14243  faclbnd4lem1  14328  bcn1  14348  hashfxnn0  14372  ccat2s1p1  14666  ccat2s1p2  14667  cats1fvn  14894  cats1fv  14895  cats1cat  14897  cats2cat  14898  wrdlen3s3  14985  sgnrn  15134  sgnclre  15138  abs3difi  15460  0.999...  15934  bpoly3  16111  ef01bndlem  16239  cos1bnd  16242  cos2bnd  16243  sin4lt0  16250  rpnnen2lem3  16271  rpnnen2lem11  16279  rpnnen  16282  rexpen  16283  aleph1irr  16301  3dvdsdec  16389  3dvds2dec  16390  divalglem2  16452  ndvdsi  16469  flodddiv4  16472  gcdaddmlem  16581  bezout  16600  3lcm2e6woprm  16672  6lcm4e12  16673  lcmf0  16691  lcmf2a3a4e12  16704  dec2dvds  17122  modxai  17127  modsubi  17131  gcdi  17132  numexp2x  17137  2exp5  17144  2exp11  17148  ex-chn2  18693  0symgefmndeq  19463  pmtrprfval  19556  m1expaddsub  19567  0frgp  19848  staffval  20923  cnfldcj  21510  cnfldds  21513  cnfldfunALT  21516  xrsadd  21519  xrsmul  21520  xrsds  21539  cnmgpid  21558  nn0srg  21566  rge0srg  21567  zring0  21587  pzriprnglem13  21622  pzriprng1ALT  21625  fermltlchr  21658  cnmsgnsubg  21706  psgninv  21711  re0g  21741  ocvfval  21795  frlmbas  21884  mdetrlin  22738  mdetunilem9  22756  leordtval2  23348  iscnp2  23375  utop3cls  24387  nmfval  24724  nmoffn  24847  nmofval  24850  icccld  24902  addcnlem  25001  iimulcn  25076  icopnfhmeo  25081  iccpnfcnv  25082  iccpnfhmeo  25083  xrhmeo  25084  xrhmph  25085  oprpiece1res1  25089  oprpiece1res2  25090  ishtpy  25110  pcoass  25162  cnstrcvs  25279  cncvs  25283  recvs  25284  qcvs  25285  zclmncvs  25286  tcphex  25355  cnfldcusp  25495  resscdrg  25496  reust  25519  recusp  25520  vitalilem4  25749  vitalilem5  25750  mbfdm  25764  dveflem  26117  dvlipcn  26132  c1lip2  26136  dgrid  26400  iaa  26465  abelthlem3  26572  abelthlem5  26574  abelth  26580  efcn  26582  sinhalfpilem  26604  sincosq1lem  26638  sincosq4sgn  26642  tangtx  26646  sincos4thpi  26654  sincos6thpi  26657  pigt3  26659  pige3ALT  26661  cos0pilt1  26673  logi  26728  relogcn  26779  dvlog2lem  26793  dvlog2  26794  logtayl  26801  logtayl2  26803  cxpsqrtlem  26843  cxpsqrt  26844  2irrexpq  26872  cxpcn2  26887  cxpcn3  26889  logblog  26933  2logb9irr  26936  2logb3irr  26938  2logb9irrALT  26939  sqrt2cxp2logb9e3  26940  2irrexpqALT  26941  ang180lem1  26950  ang180lem2  26951  1cubrlem  26982  mcubic  26988  quart1lem  26996  quart1  26997  reasinsin  27037  atancj  27051  efiatan  27053  atantan  27064  atanbndlem  27066  atan1  27069  atancn  27077  atantayl2  27079  log2cnv  27085  log2tlbnd  27086  log2ublem1  27087  log2ublem2  27088  log2ub  27090  efrlim  27110  scvxcvx  27126  1sgm2ppw  27340  ppiub  27344  bclbnd  27420  bposlem8  27431  lgsdir2lem1  27465  lgsdir2lem5  27469  lgseisenlem1  27515  lgseisenlem2  27516  lgsquadlem1  27520  chebbnd1  27612  dchrvmasumlem2  27638  norecfn  28115  norec2fn  28125  addsproplem2  28139  addsproplem6  28143  addbdaylem  28186  neg1s  28196  negsproplem2  28198  mulsproplem2  28286  mulsproplem3  28287  mulsproplem5  28289  mulsproplem6  28290  mulsproplem7  28291  mulsproplem8  28292  mulsproplem13  28297  mulsproplem14  28298  0zs  28557  zseo  28591  twocut  28592  bdaypw2n0bndlem  28632  bdaypw2bnd  28634  bdayfinbndlem1  28636  z12bdaylem2  28640  istrkg3ld  28706  trgcgrg  28760  ax5seglem7  29251  axlowdimlem6  29263  axlowdimlem8  29265  axlowdimlem11  29268  elntg2  29301  cusgrsizeindb1  29766  vtxdginducedm1  29859  0grrusgr  29895  erclwwlktr  30339  erclwwlkntr  30388  wlk2v2e  30474  upgr3v3e3cycl  30497  konigsberglem1  30569  konigsberglem2  30570  konigsberglem3  30571  konigsberglem5  30573  ex-fl  30764  ex-mod  30766  ex-hash  30770  ex-lcm  30775  0vfval  30924  smcnlem  31015  lnocoi  31075  nmlno0lem  31111  nmblolbii  31117  blocnilem  31122  blocni  31123  cncph  31137  isph  31140  ip0i  31143  ip1ilem  31144  ip2i  31146  ipdirilem  31147  ipasslem7  31154  ipasslem8  31155  ipasslem9  31156  ipasslem10  31157  ipasslem11  31158  ip2dii  31162  pythi  31168  siilem1  31169  siilem2  31170  siii  31171  hvmulassi  31364  hvmulcomi  31365  hvdistr1i  31369  hvsubdistr1i  31370  hvassi  31371  hvadd32i  31372  hvsubassi  31373  hvsub32i  31374  normlem0  31427  normlem8  31435  normlem9  31436  bcseqi  31438  polid2i  31475  hhph  31496  hlim0  31553  shscli  31635  shlessi  31695  shlej1i  31696  omlsilem  31720  shlubi  31733  h1de2i  31871  pjadjii  31992  pjaddii  31993  pjmulii  31995  pjdifnormii  32001  pjcji  32002  hoaddsubassi  32138  eigrei  32152  eigposi  32154  eigorthi  32155  adj0  32312  lnopeq0lem1  32323  lnopunilem1  32328  lnophmlem2  32335  nmcexi  32344  nmcopexi  32345  lnfn0i  32360  nmcfnexi  32369  mdexchi  32653  xppreima2  32962  dp2clq  33166  dp2lt  33170  dp2ltc  33172  dpexpp1  33193  dpmul  33198  dpmul4  33199  elxrge02  33217  xrge0adddir  33304  psgnid  33383  cnmsgn0g  33432  altgnsg  33435  xrnarchi  33470  xrge0slmod  33634  znfermltl  33647  ccfldextdgrr  34028  cos9thpiminplylem4  34141  cos9thpiminplylem5  34142  raddcn  34285  xrge0iifcnv  34289  xrge0iifiso  34291  xrge0iifhmeo  34292  xrge0iifhom  34293  xrge0iifmhm  34295  xrge0mulc1cn  34297  lmlimxrge0  34304  pnfneige0  34307  lmxrge0  34308  zringnm  34314  rezh  34325  qqh0  34340  qqh1  34341  qqhucn  34348  esumpinfval  34429  hashf2  34440  esumcvg  34442  br2base  34625  sxbrsigalem3  34628  dya2iocbrsiga  34631  dya2icobrsiga  34632  sxbrsigalem1  34641  sxbrsigalem2  34642  sxbrsigalem4  34643  sxbrsigalem5  34644  sxbrsiga  34646  ballotlem2  34845  ballotlem4  34855  ballotlemi1  34859  ballotth  34894  signstf  34919  itgexpif  34959  chtvalz  34982  hgt750lemd  35001  hgt750lem  35004  tgoldbachgnn  35012  lfuhgr2  35565  subfacp1lem1  35625  subfacp1lem6  35631  kur14lem6  35657  cvmliftlem4  35734  satf0suc  35822  problem4  36114  quad3  36116  iexpire  36181  fununiq  36215  fvtransport  36478  ttcid  36947  dfttc2g  36961  bj-minftyccb  37813  taupilem2  37910  iccioo01  37917  1oequni2o  37958  finxp1o  37982  finxpreclem4  37984  cos2h  38206  tan2h  38207  poimirlem9  38224  poimirlem27  38242  poimirlem28  38243  ismblfin  38256  mbfposadd  38262  ftc1anclem5  38292  asindmre  38298  dvasin  38299  dvacos  38300  rrnval  38422  dihjatcclem4  42141  lcmineqlem12  42753  fisdomnn  42958  subex  42961  absex  42962  cjex  42963  cxpi11d  43050  redvmptabs  43067  readvrec  43069  sn-00idlem2  43106  sn-00id  43108  remul02  43112  rabren3dioph  43490  jm2.27dlem2  43685  rmydioph  43689  rmxdioph  43691  expdiophlem2  43697  expdioph  43698  arearect  43890  areaquad  43891  2omomeqom  43978  omnord1ex  43979  corclrcl  44381  iunrelexpuztr  44393  corcltrcl  44413  dffrege76  44613  k0004val0  44828  lhe4.4ex1a  44987  binomcxplemdvbinom  45011  binomcxplemnotnn0  45014  ax6e2ndeqALT  45587  sineq0ALT  45593  nregmodelf1o  45672  pnfel0pnf  46192  lptioo2cn  46307  limsup10ex  46435  liminf10ex  46436  icccncfext  46549  itgsin0pilem1  46612  itgsbtaddcnst  46644  stoweidlem13  46675  wallispilem2  46728  wallispilem4  46730  wallispi2lem1  46733  stirlinglem13  46748  dirkerper  46758  dirkertrigeqlem3  46762  dirkeritg  46764  dirkercncflem1  46765  dirkercncflem4  46768  fourierdlem42  46811  fourierdlem62  46830  fourierdlem102  46870  fourierdlem103  46871  fourierdlem104  46872  fourierdlem114  46882  sqwvfoura  46890  fourierswlem  46892  fouriersw  46893  smfmullem4  47456  nthrucw  47550  goldracos5teq  47567  goldratmolem2  47568  ceil5half3  48028  8mod5e3  48048  fmtnoprmfac2lem1  48263  fmtno4prm  48272  3exp4mod41  48313  41prothprmlem2  48315  ppivalnn4  48324  6gbe  48481  7gbow  48482  8gbe  48483  9gbo  48484  11gbo  48485  sbgoldbalt  48491  nnsum4primesevenALTV  48511  usgrexmpl2nb0  48741  usgrexmpl2nb3  48744  gpg3nbgrvtx0  48786  gpg3nbgrvtx0ALT  48787  gpg3nbgrvtx1  48788  gpg5grlim  48803  gpg5grlic  48804  0nodd  48880  oddinmgm  48885  2zrng0  48954  zlmodzxz0  49081  zlmodzxzequa  49221  zlmodzxzequap  49224  zlmodzxzldeplem3  49227  nnlog2ge0lt1  49291  blen1  49309  blen2  49310  nnolog2flm1  49315  ackval42  49421  ehl2eudisval0  49450  line2ylem  49476  i0oii  49643  io1ii  49644  sepfsepc  49651  rescofuf  49816  setc1ohomfval  50216  setc1ocofval  50217