Theorem mp3an 1460

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 1447	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 689	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  raltp  4642  rextp  4643  opthhausdorff  5432  funopg  6475  feq12i  6602  ftp  7038  caovass  7481  caovdi  7500  ordom  7731  mptexw  7804  ofmres  7836  mpoexw  7928  omopthlem1  8498  omopthlem2  8499  omopthi  8500  xpcomen  8859  snnen2o  9035  unfilem3  9089  hartogs  9312  card2on  9322  unwf  9577  inlresf1  9682  inrresf1  9684  tskwe  9717  alephsmo  9867  dfac4  9887  dfac2a  9894  ackbij1lem13  9997  axdc2lem  10213  axcclem  10222  ondomon  10328  cfpwsdom  10349  pwfseqlem2  10424  pwfseqlem3  10425  1lt2pi  10670  addassi  10994  mulassi  10995  adddii  10996  adddiri  10997  lttri  11110  lelttri  11111  ltletri  11112  letri  11113  ltadd2i  11115  mul02lem2  11161  addid1  11164  addcani  11177  addcan2i  11178  mul12i  11179  mul32i  11180  add12i  11206  add32i  11207  subaddi  11317  subadd2i  11318  subsub23i  11320  addsubassi  11321  addsubi  11322  subcani  11323  subcan2i  11324  pnncani  11325  subdii  11433  subdiri  11434  ltadd1i  11538  leadd1i  11539  leadd2i  11540  ltsubaddi  11541  lesubaddi  11542  ltsubadd2i  11543  lesubadd2i  11544  ltaddsubi  11545  mulcani  11623  div23i  11742  div11i  11743  1mhlfehlf  12201  halfpm6th  12203  3halfnz  12408  addex  12737  mulex  12738  unirnioo  13190  ioorebas  13192  xnn0xrge0  13247  fldiv4lem1div2  13566  uzenom  13693  nnenom  13709  seqexw  13746  m1expcl2  13813  i4  13930  expnass  13933  faclbnd4lem1  14016  bcn1  14036  hashfxnn0  14060  ccat2s1p1  14345  ccat2s1p2  14346  cats1fvn  14580  cats1fv  14581  cats1cat  14583  cats2cat  14584  wrdlen3s3  14671  abs3difi  15130  0.999...  15602  bpoly3  15777  ef01bndlem  15902  cos1bnd  15905  cos2bnd  15906  sin4lt0  15913  rpnnen2lem3  15934  rpnnen2lem11  15942  rpnnen  15945  rexpen  15946  aleph1irr  15964  3dvdsdec  16050  3dvds2dec  16051  divalglem2  16113  ndvdsi  16130  flodddiv4  16131  gcdaddmlem  16240  bezout  16260  3lcm2e6woprm  16329  6lcm4e12  16330  lcmf0  16348  lcmf2a3a4e12  16361  dec2dvds  16773  modxai  16778  modsubi  16782  gcdi  16783  numexp2x  16789  2exp5  16796  2exp11  16800  0symgefmndeq  19010  pmtrprfval  19104  m1expaddsub  19115  0frgp  19394  staffval  20116  cnfldcj  20613  cnfldds  20616  cnfldfunALT  20619  cnfldfunALTOLD  20620  xrsadd  20624  xrsmul  20625  xrsds  20650  cnmgpid  20669  nn0srg  20677  rge0srg  20678  zring0  20689  cnmsgnsubg  20791  psgninv  20796  re0g  20826  ocvfval  20880  frlmbas  20971  mdetrlin  21760  mdetunilem9  21778  leordtval2  22372  iscnp2  22399  utop3cls  23412  nmfval  23753  nmoffn  23884  nmofval  23887  icccld  23939  addcnlem  24036  iimulcn  24110  icopnfhmeo  24115  iccpnfcnv  24116  iccpnfhmeo  24117  xrhmeo  24118  xrhmph  24119  oprpiece1res1  24123  oprpiece1res2  24124  ishtpy  24144  pcoass  24196  cnstrcvs  24313  cncvs  24317  recvs  24318  recvsOLD  24319  qcvs  24320  zclmncvs  24321  tcphex  24390  cnfldcusp  24530  resscdrg  24531  reust  24554  recusp  24555  vitalilem4  24784  vitalilem5  24785  mbfdm  24799  dveflem  25152  dvlipcn  25167  c1lip2  25171  dgrid  25434  iaa  25494  abelthlem3  25601  abelthlem5  25603  abelth  25609  efcn  25611  sinhalfpilem  25629  sincosq1lem  25663  sincosq4sgn  25667  tangtx  25671  sincos4thpi  25679  sincos6thpi  25681  pigt3  25683  pige3ALT  25685  cos0pilt1  25697  relogcn  25802  dvlog2lem  25816  dvlog2  25817  logtayl  25824  logtayl2  25826  cxpsqrtlem  25866  cxpsqrt  25867  2irrexpq  25894  cxpcn2  25908  cxpcn3  25910  logblog  25951  2logb9irr  25954  2logb3irr  25956  2logb9irrALT  25957  sqrt2cxp2logb9e3  25958  2irrexpqALT  25959  ang180lem1  25968  ang180lem2  25969  1cubrlem  26000  mcubic  26006  quart1lem  26014  quart1  26015  reasinsin  26055  atancj  26069  efiatan  26071  atantan  26082  atanbndlem  26084  atan1  26087  atancn  26095  atantayl2  26097  log2cnv  26103  log2tlbnd  26104  log2ublem1  26105  log2ublem2  26106  log2ub  26108  efrlim  26128  scvxcvx  26144  1sgm2ppw  26357  ppiub  26361  bclbnd  26437  bposlem8  26448  lgsdir2lem1  26482  lgsdir2lem5  26486  lgseisenlem1  26532  lgseisenlem2  26533  lgsquadlem1  26537  chebbnd1  26629  dchrvmasumlem2  26655  istrkg3ld  26831  trgcgrg  26885  ax5seglem7  27312  axlowdimlem6  27324  axlowdimlem8  27326  axlowdimlem11  27329  elntg2  27362  cusgrsizeindb1  27826  vtxdginducedm1  27919  0grrusgr  27955  erclwwlktr  28395  erclwwlkntr  28444  wlk2v2e  28530  upgr3v3e3cycl  28553  konigsberglem1  28625  konigsberglem2  28626  konigsberglem3  28627  konigsberglem5  28629  ex-fl  28820  ex-mod  28822  ex-hash  28826  ex-lcm  28831  0vfval  28977  smcnlem  29068  lnocoi  29128  nmlno0lem  29164  nmblolbii  29170  blocnilem  29175  blocni  29176  cncph  29190  isph  29193  ip0i  29196  ip1ilem  29197  ip2i  29199  ipdirilem  29200  ipasslem7  29207  ipasslem8  29208  ipasslem9  29209  ipasslem10  29210  ipasslem11  29211  ip2dii  29215  pythi  29221  siilem1  29222  siilem2  29223  siii  29224  hvmulassi  29417  hvmulcomi  29418  hvdistr1i  29422  hvsubdistr1i  29423  hvassi  29424  hvadd32i  29425  hvsubassi  29426  hvsub32i  29427  normlem0  29480  normlem8  29488  normlem9  29489  bcseqi  29491  polid2i  29528  hhph  29549  hlim0  29606  shscli  29688  shlessi  29748  shlej1i  29749  omlsilem  29773  shlubi  29786  h1de2i  29924  pjadjii  30045  pjaddii  30046  pjmulii  30048  pjdifnormii  30054  pjcji  30055  hoaddsubassi  30191  eigrei  30205  eigposi  30207  eigorthi  30208  adj0  30365  lnopeq0lem1  30376  lnopunilem1  30381  lnophmlem2  30388  nmcexi  30397  nmcopexi  30398  lnfn0i  30413  nmcfnexi  30422  mdexchi  30706  xppreima2  30997  dp2clq  31164  dp2lt  31168  dp2ltc  31170  dpexpp1  31191  dpmul  31196  dpmul4  31197  elxrge02  31215  xrge0adddir  31310  psgnid  31373  cnmsgn0g  31422  altgnsg  31425  xrnarchi  31447  xrge0slmod  31557  znfermltl  31571  ccfldextdgrr  31751  raddcn  31888  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhmeo  31895  xrge0iifhom  31896  xrge0iifmhm  31898  xrge0mulc1cn  31900  lmlimxrge0  31907  pnfneige0  31910  lmxrge0  31911  zringnm  31917  rezh  31930  qqh0  31943  qqh1  31944  qqhucn  31951  esumpinfval  32050  hashf2  32061  esumcvg  32063  br2base  32245  sxbrsigalem3  32248  dya2iocbrsiga  32251  dya2icobrsiga  32252  sxbrsigalem1  32261  sxbrsigalem2  32262  sxbrsigalem4  32263  sxbrsigalem5  32264  sxbrsiga  32266  ballotlem2  32464  ballotlem4  32474  ballotlemi1  32478  ballotth  32513  sgnclre  32515  signstf  32554  itgexpif  32595  chtvalz  32618  hgt750lemd  32637  hgt750lem  32640  tgoldbachgnn  32648  lfuhgr2  33089  subfacp1lem1  33150  subfacp1lem6  33156  kur14lem6  33182  cvmliftlem4  33259  satf0suc  33347  problem4  33635  quad3  33637  logi  33709  iexpire  33710  fununiq  33752  on2recsfn  33835  norecfn  34112  norec2fn  34122  fvtransport  34343  bj-minftyccb  35405  taupilem2  35502  iccioo01  35507  1oequni2o  35548  finxp1o  35572  finxpreclem4  35574  cos2h  35777  tan2h  35778  poimirlem9  35795  poimirlem27  35813  poimirlem28  35814  ismblfin  35827  mbfposadd  35833  ftc1anclem5  35863  asindmre  35869  dvasin  35870  dvacos  35871  rrnval  35994  el3v  36380  dihjatcclem4  39442  lcmineqlem12  40055  sn-00idlem2  40389  sn-00id  40391  remul02  40395  rei4  40412  sn-0lt1  40439  rabren3dioph  40644  jm2.27dlem2  40839  rmydioph  40843  rmxdioph  40845  expdiophlem2  40851  expdioph  40852  arearect  41053  areaquad  41054  corclrcl  41322  iunrelexpuztr  41334  corcltrcl  41354  dffrege76  41554  k0004val0  41771  lhe4.4ex1a  41954  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  ax6e2ndeqALT  42558  sineq0ALT  42564  pnfel0pnf  43073  lptioo2cn  43193  limsup10ex  43321  liminf10ex  43322  icccncfext  43435  itgsin0pilem1  43498  itgsbtaddcnst  43530  stoweidlem13  43561  wallispilem2  43614  wallispilem4  43616  wallispi2lem1  43619  stirlinglem13  43634  dirkerper  43644  dirkertrigeqlem3  43648  dirkeritg  43650  dirkercncflem1  43651  dirkercncflem4  43654  fourierdlem42  43697  fourierdlem62  43716  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem114  43768  sqwvfoura  43776  fourierswlem  43778  fouriersw  43779  smfmullem4  44339  fmtnoprmfac2lem1  45029  fmtno4prm  45038  3exp4mod41  45079  41prothprmlem2  45081  6gbe  45234  7gbow  45235  8gbe  45236  9gbo  45237  11gbo  45238  sbgoldbalt  45244  nnsum4primesevenALTV  45264  0nodd  45375  oddinmgm  45380  2zrng0  45507  zlmodzxz0  45703  zlmodzxzequa  45848  zlmodzxzequap  45851  zlmodzxzldeplem3  45854  nnlog2ge0lt1  45923  blen1  45941  blen2  45942  nnolog2flm1  45947  ackval42  46053  ehl2eudisval0  46082  line2ylem  46108  i0oii  46224  io1ii  46225  sepfsepc  46232