Theorem mp3an 1489

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  el3v  3462  raltp  4670  rextp  4671  opthhausdorff  5499  funopg  6570  feq12i  6698  ftp  7154  caovass  7612  caovdi  7631  ordom  7870  mptexw  7948  ofmres  7979  sbcoteq1a  8046  mpoexw  8073  xpord3lem  8143  omopthlem1  8643  omopthlem2  8644  omopthi  8645  on2recsfn  8651  xpcomen  9054  snnen2o  9203  unfilem3  9265  hartogs  9504  card2on  9514  unwf  9780  inlresf1  9908  inrresf1  9910  tskwe  9943  alephsmo  10093  dfac4  10113  dfac2a  10120  ackbij1lem13  10221  axdc2lem  10438  axcclem  10447  ondomon  10553  cfpwsdom  10575  pwfseqlem2  10650  pwfseqlem3  10651  1lt2pi  10896  addassi  11225  mulassi  11226  adddii  11227  adddiri  11228  lttri  11342  lelttri  11343  ltletri  11344  letri  11345  ltadd2i  11347  mul02lem2  11393  addrid  11396  addcani  11409  addcan2i  11410  mul12i  11411  mul32i  11412  add12i  11439  add32i  11440  subaddi  11551  subadd2i  11552  subsub23i  11554  addsubassi  11555  addsubi  11556  subcani  11557  subcan2i  11558  pnncani  11559  subdii  11669  subdiri  11670  ltadd1i  11774  leadd1i  11775  leadd2i  11776  ltsubaddi  11777  lesubaddi  11778  ltsubadd2i  11779  lesubadd2i  11780  ltaddsubi  11781  mulcani  11859  div23i  11979  div11i  11980  3halfnz  12681  mpoaddex  13018  addex  13019  mpomulex  13020  mulex  13021  unirnioo  13482  ioorebas  13484  xnn0xrge0  13539  fldiv4lem1div2  13877  uzenom  14007  nnenom  14023  seqexw  14060  m1expcl2  14128  i4  14247  expnass  14251  faclbnd4lem1  14336  bcn1  14356  hashfxnn0  14380  ccat2s1p1  14674  ccat2s1p2  14675  cats1fvn  14902  cats1fv  14903  cats1cat  14905  cats2cat  14906  wrdlen3s3  14993  sgnrn  15142  sgnclre  15146  abs3difi  15468  0.999...  15942  bpoly3  16118  ef01bndlem  16246  cos1bnd  16249  cos2bnd  16250  sin4lt0  16257  rpnnen2lem3  16278  rpnnen2lem11  16286  rpnnen  16289  rexpen  16290  aleph1irr  16308  3dvdsdec  16396  3dvds2dec  16397  divalglem2  16459  ndvdsi  16476  flodddiv4  16479  gcdaddmlem  16588  bezout  16607  3lcm2e6woprm  16679  6lcm4e12  16680  lcmf0  16698  lcmf2a3a4e12  16711  dec2dvds  17129  modxai  17134  modsubi  17138  gcdi  17139  numexp2x  17144  2exp5  17151  2exp11  17155  ex-chn2  18700  0symgefmndeq  19470  pmtrprfval  19563  m1expaddsub  19574  0frgp  19855  staffval  20955  cnfldcj  21542  cnfldds  21545  cnfldfunALT  21548  xrsadd  21551  xrsmul  21552  xrsds  21571  cnmgpid  21590  nn0srg  21598  rge0srg  21599  zring0  21619  pzriprnglem13  21654  pzriprng1ALT  21657  fermltlchr  21690  cnmsgnsubg  21738  psgninv  21743  re0g  21773  ocvfval  21827  frlmbas  21916  mdetrlin  22770  mdetunilem9  22788  leordtval2  23380  iscnp2  23407  utop3cls  24419  nmfval  24756  nmoffn  24879  nmofval  24882  icccld  24934  addcnlem  25033  iimulcn  25108  icopnfhmeo  25113  iccpnfcnv  25114  iccpnfhmeo  25115  xrhmeo  25116  xrhmph  25117  oprpiece1res1  25121  oprpiece1res2  25122  ishtpy  25142  pcoass  25194  cnstrcvs  25311  cncvs  25315  recvs  25316  qcvs  25317  zclmncvs  25318  tcphex  25387  cnfldcusp  25527  resscdrg  25528  reust  25551  recusp  25552  vitalilem4  25781  vitalilem5  25782  mbfdm  25796  dveflem  26149  dvlipcn  26164  c1lip2  26168  dgrid  26432  iaa  26499  abelthlem3  26607  abelthlem5  26609  abelth  26615  efcn  26617  sinhalfpilem  26639  sincosq1lem  26673  sincosq4sgn  26677  tangtx  26681  sincos4thpi  26689  sincos6thpi  26692  pigt3  26694  pige3ALT  26696  cos0pilt1  26708  logi  26763  relogcn  26814  dvlog2lem  26828  dvlog2  26829  logtayl  26836  logtayl2  26838  cxpsqrtlem  26878  cxpsqrt  26879  2irrexpq  26907  cxpcn2  26922  cxpcn3  26924  logblog  26968  2logb9irr  26971  2logb3irr  26973  2logb9irrALT  26974  sqrt2cxp2logb9e3  26975  2irrexpqALT  26976  ang180lem1  26985  ang180lem2  26986  1cubrlem  27017  mcubic  27023  quart1lem  27031  quart1  27032  reasinsin  27072  atancj  27086  efiatan  27088  atantan  27099  atanbndlem  27101  atan1  27104  atancn  27112  atantayl2  27114  log2cnv  27120  log2tlbnd  27121  log2ublem1  27122  log2ublem2  27123  log2ub  27125  efrlim  27145  scvxcvx  27161  1sgm2ppw  27375  ppiub  27379  bclbnd  27455  bposlem8  27466  lgsdir2lem1  27500  lgsdir2lem5  27504  lgseisenlem1  27550  lgseisenlem2  27551  lgsquadlem1  27555  chebbnd1  27647  dchrvmasumlem2  27673  norecfn  28150  norec2fn  28160  addsproplem2  28174  addsproplem6  28178  addbdaylem  28221  neg1s  28231  negsproplem2  28233  mulsproplem2  28321  mulsproplem3  28322  mulsproplem5  28324  mulsproplem6  28325  mulsproplem7  28326  mulsproplem8  28327  mulsproplem13  28332  mulsproplem14  28333  0zs  28592  zseo  28626  twocut  28627  bdaypw2n0bndlem  28667  bdaypw2bnd  28669  bdayfinbndlem1  28671  z12bdaylem2  28675  istrkg3ld  28741  trgcgrg  28795  ax5seglem7  29296  axlowdimlem6  29308  axlowdimlem8  29310  axlowdimlem11  29313  elntg2  29346  cusgrsizeindb1  29811  vtxdginducedm1  29904  0grrusgr  29940  erclwwlktr  30384  erclwwlkntr  30433  wlk2v2e  30519  upgr3v3e3cycl  30542  konigsberglem1  30614  konigsberglem2  30615  konigsberglem3  30616  konigsberglem5  30618  ex-fl  30809  ex-mod  30811  ex-hash  30815  ex-lcm  30820  0vfval  30969  smcnlem  31060  lnocoi  31120  nmlno0lem  31156  nmblolbii  31162  blocnilem  31167  blocni  31168  cncph  31182  isph  31185  ip0i  31188  ip1ilem  31189  ip2i  31191  ipdirilem  31192  ipasslem7  31199  ipasslem8  31200  ipasslem9  31201  ipasslem10  31202  ipasslem11  31203  ip2dii  31207  pythi  31213  siilem1  31214  siilem2  31215  siii  31216  hvmulassi  31409  hvmulcomi  31410  hvdistr1i  31414  hvsubdistr1i  31415  hvassi  31416  hvadd32i  31417  hvsubassi  31418  hvsub32i  31419  normlem0  31472  normlem8  31480  normlem9  31481  bcseqi  31483  polid2i  31520  hhph  31541  hlim0  31598  shscli  31680  shlessi  31740  shlej1i  31741  omlsilem  31765  shlubi  31778  h1de2i  31916  pjadjii  32037  pjaddii  32038  pjmulii  32040  pjdifnormii  32046  pjcji  32047  hoaddsubassi  32183  eigrei  32197  eigposi  32199  eigorthi  32200  adj0  32357  lnopeq0lem1  32368  lnopunilem1  32373  lnophmlem2  32380  nmcexi  32389  nmcopexi  32390  lnfn0i  32405  nmcfnexi  32414  mdexchi  32698  xppreima2  33007  dp2clq  33211  dp2lt  33215  dp2ltc  33217  dpexpp1  33238  dpmul  33243  dpmul4  33244  elxrge02  33262  xrge0adddir  33347  psgnid  33426  cnmsgn0g  33475  altgnsg  33478  xrnarchi  33513  xrge0slmod  33677  znfermltl  33690  ccfldextdgrr  34071  cos9thpiminplylem4  34184  cos9thpiminplylem5  34185  raddcn  34328  xrge0iifcnv  34332  xrge0iifiso  34334  xrge0iifhmeo  34335  xrge0iifhom  34336  xrge0iifmhm  34338  xrge0mulc1cn  34340  lmlimxrge0  34347  pnfneige0  34350  lmxrge0  34351  zringnm  34357  rezh  34368  qqh0  34383  qqh1  34384  qqhucn  34391  esumpinfval  34472  hashf2  34483  esumcvg  34485  br2base  34668  sxbrsigalem3  34671  dya2iocbrsiga  34674  dya2icobrsiga  34675  sxbrsigalem1  34684  sxbrsigalem2  34685  sxbrsigalem4  34686  sxbrsigalem5  34687  sxbrsiga  34689  ballotlem2  34888  ballotlem4  34898  ballotlemi1  34902  ballotth  34937  signstf  34962  itgexpif  35002  chtvalz  35025  hgt750lemd  35044  hgt750lem  35047  tgoldbachgnn  35055  lfuhgr2  35619  subfacp1lem1  35679  subfacp1lem6  35685  kur14lem6  35711  cvmliftlem4  35788  satf0suc  35876  problem4  36168  quad3  36170  iexpire  36235  fununiq  36269  fvtransport  36532  ttcid  37031  dfttc2g  37045  bj-minftyccb  37897  taupilem2  37994  iccioo01  38001  1oequni2o  38042  finxp1o  38066  finxpreclem4  38068  cos2h  38290  tan2h  38291  poimirlem9  38308  poimirlem27  38326  poimirlem28  38327  ismblfin  38340  mbfposadd  38346  ftc1anclem5  38376  asindmre  38382  dvasin  38383  dvacos  38384  rrnval  38506  dihjatcclem4  42223  lcmineqlem12  42835  fisdomnn  43040  subex  43043  absex  43044  cjex  43045  cxpi11d  43132  redvmptabs  43149  readvrec  43151  sn-00idlem2  43188  sn-00id  43190  remul02  43194  rabren3dioph  43570  jm2.27dlem2  43765  rmydioph  43769  rmxdioph  43771  expdiophlem2  43777  expdioph  43778  arearect  43970  areaquad  43971  2omomeqom  44058  omnord1ex  44059  corclrcl  44461  iunrelexpuztr  44473  corcltrcl  44493  dffrege76  44693  k0004val0  44908  lhe4.4ex1a  45067  binomcxplemdvbinom  45091  binomcxplemnotnn0  45094  ax6e2ndeqALT  45667  sineq0ALT  45673  nregmodelf1o  45752  pnfel0pnf  46272  lptioo2cn  46387  limsup10ex  46515  liminf10ex  46516  icccncfext  46629  itgsin0pilem1  46692  itgsbtaddcnst  46724  stoweidlem13  46755  wallispilem2  46808  wallispilem4  46810  wallispi2lem1  46813  stirlinglem13  46828  dirkerper  46838  dirkertrigeqlem3  46842  dirkeritg  46844  dirkercncflem1  46845  dirkercncflem4  46848  fourierdlem42  46891  fourierdlem62  46910  fourierdlem102  46950  fourierdlem103  46951  fourierdlem104  46952  fourierdlem114  46962  sqwvfoura  46970  fourierswlem  46972  fouriersw  46973  smfmullem4  47536  sqrtnnaa  47632  sqrtnzqaa  47633  goldracos5teq  47650  goldratmolem2  47651  ceil5half3  48111  8mod5e3  48131  fmtnoprmfac2lem1  48346  fmtno4prm  48355  3exp4mod41  48396  41prothprmlem2  48398  ppivalnn4  48407  6gbe  48564  7gbow  48565  8gbe  48566  9gbo  48567  11gbo  48568  sbgoldbalt  48574  nnsum4primesevenALTV  48594  usgrexmpl2nb0  48824  usgrexmpl2nb3  48827  gpg3nbgrvtx0  48869  gpg3nbgrvtx0ALT  48870  gpg3nbgrvtx1  48871  gpg5grlim  48886  gpg5grlic  48887  0nodd  48963  oddinmgm  48968  2zrng0  49037  zlmodzxz0  49164  zlmodzxzequa  49304  zlmodzxzequap  49307  zlmodzxzldeplem3  49310  nnlog2ge0lt1  49374  blen1  49392  blen2  49393  nnolog2flm1  49398  ackval42  49504  ehl2eudisval0  49533  line2ylem  49559  i0oii  49726  io1ii  49727  sepfsepc  49734  rescofuf  49899  setc1ohomfval  50299  setc1ocofval  50300  crossp3i  50676