Theorem mp3an 1490

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

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

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 402  df-3an 1105

This theorem is used by:  el3v  3458  raltp  4666  rextp  4667  opthhausdorff  5487  funopg  6563  feq12i  6691  ftp  7150  caovass  7610  caovdi  7629  ordom  7871  mptexw  7949  ofmres  7980  sbcoteq1a  8046  mpoexw  8075  xpord3lem  8145  omopthlem1  8647  omopthlem2  8648  omopthi  8649  on2recsfn  8655  xpcomen  9066  snnen2o  9215  unfilem3  9277  hartogs  9516  card2on  9526  unwf  9792  inlresf1  9953  inrresf1  9955  tskwe  9988  alephsmo  10138  dfac4  10158  dfac2a  10165  ackbij1lem13  10266  axdc2lem  10483  axcclem  10492  ondomon  10604  cfpwsdom  10626  pwfseqlem2  10701  pwfseqlem3  10702  1lt2pi  10947  addassi  11276  mulassi  11277  adddii  11278  adddiri  11279  lttri  11393  lelttri  11394  ltletri  11395  letri  11396  ltadd2i  11398  mul02lem2  11444  addrid  11447  addcani  11460  addcan2i  11461  mul12i  11462  mul32i  11463  add12i  11490  add32i  11491  subaddi  11602  subadd2i  11603  subsub23i  11605  addsubassi  11606  addsubi  11607  subcani  11608  subcan2i  11609  pnncani  11610  subdii  11720  subdiri  11721  ltadd1i  11825  leadd1i  11826  leadd2i  11827  ltsubaddi  11828  lesubaddi  11829  ltsubadd2i  11830  lesubadd2i  11831  ltaddsubi  11832  mulcani  11910  div23i  12030  div11i  12031  3halfnz  12733  mpoaddex  13071  addex  13072  mpomulex  13073  mulex  13074  unirnioo  13535  ioorebas  13537  xnn0xrge0  13592  fldiv4lem1div2  13931  uzenom  14061  nnenom  14077  seqexw  14114  m1expcl2  14182  i4  14301  expnass  14305  faclbnd4lem1  14390  bcn1  14410  hashfxnn0  14434  ccat2s1p1  14730  ccat2s1p2  14731  cats1fvn  14962  cats1fv  14963  cats1cat  14965  cats2cat  14966  wrdlen3s3  15053  sgnrn  15204  sgnclre  15208  abs3difi  15530  0.999...  16003  bpoly3  16177  ef01bndlem  16305  cos1bnd  16308  cos2bnd  16309  sin4lt0  16316  rpnnen2lem3  16337  rpnnen2lem11  16345  rpnnen  16348  rexpen  16349  aleph1irr  16367  3dvdsdec  16455  3dvds2dec  16456  divalglem2  16518  ndvdsi  16535  flodddiv4  16538  gcdaddmlem  16647  bezout  16666  3lcm2e6woprm  16738  6lcm4e12  16739  lcmf0  16757  lcmf2a3a4e12  16770  dec2dvds  17188  modxai  17193  modsubi  17197  gcdi  17198  numexp2x  17203  2exp5  17210  2exp11  17214  ex-chn2  18759  degenmgmnfn  19083  degenmgm  19084  degenmgm2opdm  19085  degenmgm2  19087  0symgefmndeq  19555  pmtrprfval  19648  m1expaddsub  19659  0frgp  19940  staffval  21045  cnfldcj  21634  cnfldds  21637  cnfldfunALT  21640  xrsadd  21643  xrsmul  21644  xrsds  21663  cnmgpid  21682  nn0srg  21690  rge0srg  21691  zring0  21711  pzriprnglem13  21746  pzriprng1ALT  21749  fermltlchr  21782  cnmsgnsubg  21830  psgninv  21835  re0g  21865  ocvfval  21919  frlmbas  22008  mdetrlin  22864  mdetunilem9  22882  leordtval2  23477  iscnp2  23504  utop3cls  24517  nmfval  24854  nmoffn  24977  nmofval  24980  icccld  25032  addcnlem  25131  iimulcn  25206  icopnfhmeo  25211  iccpnfcnv  25212  iccpnfhmeo  25213  xrhmeo  25214  xrhmph  25215  oprpiece1res1  25219  oprpiece1res2  25220  ishtpy  25240  pcoass  25292  cnstrcvs  25409  cncvs  25413  recvs  25414  qcvs  25415  zclmncvs  25416  tcphex  25485  cnfldcusp  25625  resscdrg  25626  reust  25649  recusp  25650  vitalilem4  25879  vitalilem5  25880  mbfdm  25894  dveflem  26246  dvlipcn  26261  c1lip2  26265  dgrid  26530  iaa  26600  iaaOLD  26601  abelthlem3  26709  abelthlem5  26711  abelth  26717  efcn  26719  sinhalfpilem  26741  sincosq1lem  26775  sincosq4sgn  26779  tangtx  26783  sincos4thpi  26791  sincos6thpi  26793  pigt3  26795  pige3ALT  26797  cos0pilt1  26809  logi  26864  relogcn  26915  dvlog2lem  26929  dvlog2  26930  logtayl  26937  logtayl2  26939  cxpsqrtlem  26979  cxpsqrt  26980  2irrexpq  27008  cxpcn2  27023  cxpcn3  27025  logblog  27069  2logb9irr  27072  2logb3irr  27074  2logb9irrALT  27075  sqrt2cxp2logb9e3  27076  2irrexpqALT  27077  ang180lem1  27086  ang180lem2  27087  1cubrlem  27118  mcubic  27124  quart1lem  27132  quart1  27133  reasinsin  27173  atancj  27187  efiatan  27189  atantan  27200  atanbndlem  27202  atan1  27205  atancn  27213  atantayl2  27215  log2cnv  27221  log2tlbnd  27222  log2ublem1  27223  log2ublem2  27224  log2ub  27226  efrlim  27246  scvxcvx  27262  1sgm2ppw  27476  ppiub  27480  bclbnd  27556  bposlem8  27567  lgsdir2lem1  27601  lgsdir2lem5  27605  lgseisenlem1  27651  lgseisenlem2  27652  lgsquadlem1  27656  chebbnd1  27748  dchrvmasumlem2  27774  norecfn  28251  norec2fn  28261  addsproplem2  28275  addsproplem6  28279  addbdaylem  28322  neg1s  28332  negsproplem2  28334  mulsproplem2  28422  mulsproplem3  28423  mulsproplem5  28425  mulsproplem6  28426  mulsproplem7  28427  mulsproplem8  28428  mulsproplem13  28433  mulsproplem14  28434  0zs  28693  zseo  28727  twocut  28728  bdaypw2n0bndlem  28768  bdaypw2bnd  28770  bdayfinbndlem1  28772  z12bdaylem2  28776  istrkg3ld  28842  trgcgrg  28897  ax5seglem7  29432  axlowdimlem6  29444  axlowdimlem8  29446  axlowdimlem11  29449  elntg2  29482  lfuhgr2  29646  cusgrsizeindb1  29950  vtxdginducedm1  30043  0grrusgr  30079  erclwwlktr  30532  erclwwlkntr  30581  wlk2v2e  30677  upgr3v3e3cycl  30700  konigsberglem1  30772  konigsberglem2  30773  konigsberglem3  30774  konigsberglem5  30776  ex-fl  30967  ex-mod  30969  ex-hash  30973  ex-lcm  30978  0vfval  31127  smcnlem  31218  lnocoi  31278  nmlno0lem  31314  nmblolbii  31320  blocnilem  31325  blocni  31326  cncph  31340  isph  31343  ip0i  31346  ip1ilem  31347  ip2i  31349  ipdirilem  31350  ipasslem7  31357  ipasslem8  31358  ipasslem9  31359  ipasslem10  31360  ipasslem11  31361  ip2dii  31365  pythi  31371  siilem1  31372  siilem2  31373  siii  31374  hvmulassi  31567  hvmulcomi  31568  hvdistr1i  31572  hvsubdistr1i  31573  hvassi  31574  hvadd32i  31575  hvsubassi  31576  hvsub32i  31577  normlem0  31630  normlem8  31638  normlem9  31639  bcseqi  31641  polid2i  31678  hhph  31699  hlim0  31756  shscli  31838  shlessi  31898  shlej1i  31899  omlsilem  31923  shlubi  31936  h1de2i  32074  pjadjii  32195  pjaddii  32196  pjmulii  32198  pjdifnormii  32204  pjcji  32205  hoaddsubassi  32341  eigrei  32355  eigposi  32357  eigorthi  32358  adj0  32515  lnopeq0lem1  32526  lnopunilem1  32531  lnophmlem2  32538  nmcexi  32547  nmcopexi  32548  lnfn0i  32563  nmcfnexi  32572  mdexchi  32856  xppreima2  33164  dp2clq  33366  dp2lt  33370  dp2ltc  33372  dpexpp1  33393  dpmul  33398  dpmul4  33399  elxrge02  33417  xrge0adddir  33498  psgnid  33577  cnmsgn0g  33626  altgnsg  33629  xrnarchi  33664  xrge0slmod  33828  znfermltl  33841  ccfldextdgrr  34223  cos9thpiminplylem4  34336  cos9thpiminplylem5  34337  raddcn  34480  xrge0iifcnv  34484  xrge0iifiso  34486  xrge0iifhmeo  34487  xrge0iifhom  34488  xrge0iifmhm  34490  xrge0mulc1cn  34492  lmlimxrge0  34499  pnfneige0  34502  lmxrge0  34503  zringnm  34509  rezh  34520  qqh0  34535  qqh1  34536  qqhucn  34543  esumpinfval  34624  hashf2  34635  esumcvg  34637  br2base  34821  sxbrsigalem3  34824  dya2iocbrsiga  34827  dya2icobrsiga  34828  sxbrsigalem1  34837  sxbrsigalem2  34838  sxbrsigalem4  34839  sxbrsigalem5  34840  sxbrsiga  34842  ballotlem2  35041  ballotlem4  35051  ballotlemi1  35055  ballotth  35090  signstf  35115  itgexpif  35155  chtvalz  35178  hgt750lemd  35197  hgt750lem  35200  tgoldbachgnn  35208  subfacp1lem1  35859  subfacp1lem6  35865  kur14lem6  35891  cvmliftlem4  35968  satf0suc  36056  problem4  36348  quad3  36350  iexpire  36415  fununiq  36449  fvtransport  36713  ttcid  37196  dfttc2g  37210  bj-minftyccb  38060  taupilem2  38157  iccioo01  38164  1oequni2o  38205  finxp1o  38229  finxpreclem4  38231  cos2h  38448  tan2h  38449  poimirlem9  38461  poimirlem27  38479  poimirlem28  38480  ismblfin  38493  mbfposadd  38499  ftc1anclem5  38529  asindmre  38535  dvasin  38536  dvacos  38537  rrnval  38675  dihjatcclem4  42392  lcmineqlem12  43004  fisdomnn  43209  subex  43212  absex  43213  cjex  43214  cxpi11d  43316  redvmptabs  43333  readvrec  43335  sn-00idlem2  43372  sn-00id  43374  remul02  43378  rabren3dioph  43754  jm2.27dlem2  43949  rmydioph  43953  rmxdioph  43955  expdiophlem2  43961  expdioph  43962  arearect  44154  areaquad  44155  2omomeqom  44242  omnord1ex  44243  corclrcl  44645  iunrelexpuztr  44657  corcltrcl  44677  dffrege76  44877  k0004val0  45092  lhe4.4ex1a  45251  binomcxplemdvbinom  45275  binomcxplemnotnn0  45278  ax6e2ndeqALT  45851  sineq0ALT  45857  nregmodelf1o  45936  pnfel0pnf  46456  lptioo2cn  46571  limsup10ex  46699  liminf10ex  46700  icccncfext  46813  itgsin0pilem1  46876  itgsbtaddcnst  46908  stoweidlem13  46939  wallispilem2  46992  wallispilem4  46994  wallispi2lem1  46997  stirlinglem13  47012  dirkerper  47022  dirkertrigeqlem3  47026  dirkeritg  47028  dirkercncflem1  47029  dirkercncflem4  47032  fourierdlem42  47075  fourierdlem62  47094  fourierdlem102  47134  fourierdlem103  47135  fourierdlem104  47136  fourierdlem114  47146  sqwvfoura  47154  fourierswlem  47156  fouriersw  47157  smfmullem4  47720  sqrtnnaa  47829  sqrtnzqaa  47830  goldpolyfactor  47843  goldracos5teq  47848  goldratmolem2  47849  goldratval  47852  sqrtnpoly  47859  ceil5half3  48332  8mod5e3  48352  fmtnoprmfac2lem1  48567  fmtno4prm  48576  3exp4mod41  48617  41prothprmlem2  48619  ppivalnn4  48628  6gbe  48785  7gbow  48786  8gbe  48787  9gbo  48788  11gbo  48789  sbgoldbalt  48795  nnsum4primesevenALTV  48815  usgrexmpl2nb0  49045  usgrexmpl2nb3  49048  gpg3nbgrvtx0  49090  gpg3nbgrvtx0ALT  49091  gpg3nbgrvtx1  49092  gpg5grlim  49107  gpg5grlic  49108  0nodd  49183  oddinmgm  49188  2zrng0  49257  zlmodzxz0  49384  zlmodzxzequa  49524  zlmodzxzequap  49527  zlmodzxzldeplem3  49530  nnlog2ge0lt1  49594  blen1  49612  blen2  49613  nnolog2flm1  49618  ackval42  49724  ehl2eudisval0  49753  line2ylem  49779  i0oii  49944  io1ii  49945  sepfsepc  49952  rescofuf  50117  setc1ohomfval  50517  setc1ocofval  50518