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  4665  rextp  4666  opthhausdorff  5489  fununiq  6555  funopg  6574  feq12i  6702  ftp  7161  caovass  7621  caovdi  7640  ordom  7887  mptexw  7965  ofmres  7996  sbcoteq1a  8062  mpoexw  8091  xpord3lem  8166  omopthlem1  8668  omopthlem2  8669  omopthi  8670  on2recsfn  8676  xpcomen  9087  snnen2o  9236  unfilem3  9299  hartogs  9538  card2on  9548  unwf  9818  inlresf1  9996  inrresf1  9998  tskwe  10031  alephsmo  10181  dfac4  10201  dfac2a  10208  ackbij1lem13  10309  axdc2lem  10526  axcclem  10535  ondomon  10647  cfpwsdom  10669  pwfseqlem2  10744  pwfseqlem3  10745  1lt2pi  10990  addassi  11319  mulassi  11320  adddii  11321  adddiri  11322  lttri  11436  lelttri  11437  ltletri  11438  letri  11439  ltadd2i  11441  mul02lem2  11487  addrid  11490  addcani  11503  addcan2i  11504  mul12i  11505  mul32i  11506  add12i  11533  add32i  11534  subaddi  11645  subadd2i  11646  subsub23i  11648  addsubassi  11649  addsubi  11650  subcani  11651  subcan2i  11652  pnncani  11653  subdii  11765  subdiri  11766  ltadd1i  11870  leadd1i  11871  leadd2i  11872  ltsubaddi  11873  lesubaddi  11874  ltsubadd2i  11875  lesubadd2i  11876  ltaddsubi  11877  mulcani  11955  div23i  12075  div11i  12076  3halfnz  12778  mpoaddex  13116  addex  13117  mpomulex  13118  mulex  13119  unirnioo  13580  ioorebas  13582  xnn0xrge0  13637  fldiv4lem1div2  13977  uzenom  14107  nnenom  14123  seqexw  14160  m1expcl2  14228  i4  14348  expnass  14352  faclbnd4lem1  14437  bcn1  14457  hashfxnn0  14481  ccat2s1p1  14777  ccat2s1p2  14778  cats1fvn  15009  cats1fv  15010  cats1cat  15012  cats2cat  15013  wrdlen3s3  15100  sgnrn  15251  sgnclre  15255  abs3difi  15577  0.999...  16050  bpoly3  16224  ef01bndlem  16352  cos1bnd  16355  cos2bnd  16356  sin4lt0  16363  rpnnen2lem3  16384  rpnnen2lem11  16392  rpnnen  16395  rexpen  16396  aleph1irr  16414  3dvdsdec  16502  3dvds2dec  16503  divalglem2  16565  ndvdsi  16582  flodddiv4  16585  gcdaddmlem  16696  bezout  16716  3lcm2e6woprm  16790  6lcm4e12  16791  lcmf0  16809  lcmf2a3a4e12  16822  dec2dvds  17241  modxai  17246  modsubi  17250  gcdi  17251  numexp2x  17256  2exp5  17263  2exp11  17267  ex-chn2  18812  degenmgmnfn  19136  degenmgm  19137  degenmgm2opdm  19138  degenmgm2  19140  0symgefmndeq  19608  pmtrprfval  19701  m1expaddsub  19712  0frgp  19993  staffval  21098  cnfldcj  21687  cnfldds  21690  cnfldfunALT  21693  xrsadd  21696  xrsmul  21697  xrsds  21716  cnmgpid  21735  nn0srg  21743  rge0srg  21744  zring0  21764  pzriprnglem13  21799  pzriprng1ALT  21802  fermltlchr  21835  cnmsgnsubg  21883  psgninv  21888  re0g  21918  ocvfval  21972  frlmbas  22061  mdetrlin  22917  mdetunilem9  22935  leordtval2  23530  iscnp2  23557  utop3cls  24570  nmfval  24907  nmoffn  25030  nmofval  25033  icccld  25085  addcnlem  25184  iimulcn  25259  icopnfhmeo  25264  iccpnfcnv  25265  iccpnfhmeo  25266  xrhmeo  25267  xrhmph  25268  oprpiece1res1  25272  oprpiece1res2  25273  ishtpy  25293  pcoass  25345  cnstrcvs  25462  cncvs  25466  recvs  25467  qcvs  25468  zclmncvs  25469  tcphex  25538  cnfldcusp  25678  resscdrg  25679  reust  25702  recusp  25703  vitalilem4  25932  vitalilem5  25933  mbfdm  25947  dveflem  26299  dvlipcn  26314  c1lip2  26318  dgrid  26583  iaa  26651  iaaOLD  26652  abelthlem3  26760  abelthlem5  26762  abelth  26768  efcn  26770  sinhalfpilem  26792  sincosq1lem  26826  sincosq4sgn  26830  tangtx  26834  sincos4thpi  26842  sincos6thpi  26844  pigt3  26846  pige3ALT  26848  cos0pilt1  26860  logi  26915  relogcn  26966  dvlog2lem  26980  dvlog2  26981  logtayl  26988  logtayl2  26990  cxpsqrtlem  27030  cxpsqrt  27031  2irrexpq  27059  cxpcn2  27074  cxpcn3  27076  logblog  27120  2logb9irr  27123  2logb3irr  27125  2logb9irrALT  27126  sqrt2cxp2logb9e3  27127  2irrexpqALT  27128  ang180lem1  27137  ang180lem2  27138  1cubrlem  27169  mcubic  27175  quart1lem  27183  quart1  27184  reasinsin  27224  atancj  27238  efiatan  27240  atantan  27251  atanbndlem  27253  atan1  27256  atancn  27264  atantayl2  27266  log2cnv  27272  log2tlbnd  27273  log2ublem1  27274  log2ublem2  27275  log2ub  27277  efrlim  27297  scvxcvx  27313  1sgm2ppw  27527  ppiub  27531  bclbnd  27607  bposlem8  27618  lgsdir2lem1  27652  lgsdir2lem5  27656  lgseisenlem1  27702  lgseisenlem2  27703  lgsquadlem1  27707  chebbnd1  27799  dchrvmasumlem2  27825  norecfn  28332  norec2fn  28342  addsproplem2  28356  addsproplem6  28360  addbdaylem  28403  neg1s  28413  negsproplem2  28415  mulsproplem2  28503  mulsproplem3  28504  mulsproplem5  28506  mulsproplem6  28507  mulsproplem7  28508  mulsproplem8  28509  mulsproplem13  28514  mulsproplem14  28515  0zs  28774  zseo  28808  twocut  28809  bdaypw2n0bndlem  28849  bdaypw2bnd  28851  bdayfinbndlem1  28853  z12bdaylem2  28857  istrkg3ld  28923  trgcgrg  28978  ax5seglem7  29513  axlowdimlem6  29525  axlowdimlem8  29527  axlowdimlem11  29530  elntg2  29563  lfuhgr2  29727  cusgrsizeindb1  30031  vtxdginducedm1  30124  0grrusgr  30160  erclwwlktr  30613  erclwwlkntr  30662  wlk2v2e  30758  upgr3v3e3cycl  30781  konigsberglem1  30853  konigsberglem2  30854  konigsberglem3  30855  konigsberglem5  30857  ex-fl  31048  ex-mod  31050  ex-hash  31054  ex-lcm  31059  0vfval  31208  smcnlem  31299  lnocoi  31359  nmlno0lem  31395  nmblolbii  31401  blocnilem  31406  blocni  31407  cncph  31421  isph  31424  ip0i  31427  ip1ilem  31428  ip2i  31430  ipdirilem  31431  ipasslem7  31438  ipasslem8  31439  ipasslem9  31440  ipasslem10  31441  ipasslem11  31442  ip2dii  31446  pythi  31452  siilem1  31453  siilem2  31454  siii  31455  hvmulassi  31648  hvmulcomi  31649  hvdistr1i  31653  hvsubdistr1i  31654  hvassi  31655  hvadd32i  31656  hvsubassi  31657  hvsub32i  31658  normlem0  31711  normlem8  31719  normlem9  31720  bcseqi  31722  polid2i  31759  hhph  31780  hlim0  31837  shscli  31919  shlessi  31979  shlej1i  31980  omlsilem  32004  shlubi  32017  h1de2i  32155  pjadjii  32276  pjaddii  32277  pjmulii  32279  pjdifnormii  32285  pjcji  32286  hoaddsubassi  32422  eigrei  32436  eigposi  32438  eigorthi  32439  adj0  32596  lnopeq0lem1  32607  lnopunilem1  32612  lnophmlem2  32619  nmcexi  32628  nmcopexi  32629  lnfn0i  32644  nmcfnexi  32653  mdexchi  32937  xppreima2  33245  dp2clq  33447  dp2lt  33451  dp2ltc  33453  dpexpp1  33474  dpmul  33479  dpmul4  33480  elxrge02  33498  xrge0adddir  33579  psgnid  33658  cnmsgn0g  33707  altgnsg  33710  xrnarchi  33745  xrge0slmod  33909  znfermltl  33922  ccfldextdgrr  34304  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  raddcn  34561  xrge0iifcnv  34565  xrge0iifiso  34567  xrge0iifhmeo  34568  xrge0iifhom  34569  xrge0iifmhm  34571  xrge0mulc1cn  34573  lmlimxrge0  34580  pnfneige0  34583  lmxrge0  34584  zringnm  34590  rezh  34601  qqh0  34616  qqh1  34617  qqhucn  34624  esumpinfval  34705  hashf2  34716  esumcvg  34718  br2base  34901  sxbrsigalem3  34904  dya2iocbrsiga  34907  dya2icobrsiga  34908  sxbrsigalem1  34917  sxbrsigalem2  34918  sxbrsigalem4  34919  sxbrsigalem5  34920  sxbrsiga  34922  ballotlem2  35121  ballotlem4  35131  ballotlemi1  35135  ballotth  35170  signstf  35195  itgexpif  35235  chtvalz  35258  hgt750lemd  35277  hgt750lem  35280  tgoldbachgnn  35288  subfacp1lem1  35944  subfacp1lem6  35950  kur14lem6  35976  cvmliftlem4  36053  satf0suc  36141  problem4  36433  quad3  36435  iexpire  36500  fvtransport  36797  ttcid  37280  dfttc2g  37294  bj-minftyccb  38147  taupilem2  38244  iccioo01  38251  1oequni2o  38292  finxp1o  38316  finxpreclem4  38318  cos2h  38535  tan2h  38536  poimirlem9  38548  poimirlem27  38566  poimirlem28  38567  ismblfin  38580  mbfposadd  38586  ftc1anclem5  38616  asindmre  38622  dvasin  38623  dvacos  38624  rrnval  38762  dihjatcclem4  42479  lcmineqlem12  43091  fisdomnn  43296  subex  43299  absex  43300  cjex  43301  cxpi11d  43395  redvmptabs  43412  readvrec  43414  sn-00idlem2  43451  sn-00id  43453  remul02  43457  rabren3dioph  43822  jm2.27dlem2  44017  rmydioph  44021  rmxdioph  44023  expdiophlem2  44029  expdioph  44030  arearect  44217  areaquad  44218  2omomeqom  44305  omnord1ex  44306  corclrcl  44707  iunrelexpuztr  44719  corcltrcl  44739  dffrege76  44939  k0004val0  45154  lhe4.4ex1a  45313  binomcxplemdvbinom  45337  binomcxplemnotnn0  45340  ax6e2ndeqALT  45913  sineq0ALT  45919  nregmodelf1o  46005  pnfel0pnf  46540  lptioo2cn  46655  limsup10ex  46783  liminf10ex  46784  icccncfext  46897  itgsin0pilem1  46960  itgsbtaddcnst  46992  stoweidlem13  47023  wallispilem2  47076  wallispilem4  47078  wallispi2lem1  47081  stirlinglem13  47096  dirkerper  47106  dirkertrigeqlem3  47110  dirkeritg  47112  dirkercncflem1  47113  dirkercncflem4  47116  fourierdlem42  47159  fourierdlem62  47178  fourierdlem102  47218  fourierdlem103  47219  fourierdlem104  47220  fourierdlem114  47230  sqwvfoura  47238  fourierswlem  47240  fouriersw  47241  smfmullem4  47804  sqrtnnaa  47913  sqrtnzqaa  47914  goldpolyfactor  47927  goldracos5teq  47932  goldratmolem2  47933  goldratval  47936  sqrtnpoly  47943  ceil5half3  48416  8mod5e3  48436  fmtnoprmfac2lem1  48651  fmtno4prm  48660  3exp4mod41  48701  41prothprmlem2  48703  ppivalnn4  48712  6gbe  48869  7gbow  48870  8gbe  48871  9gbo  48872  11gbo  48873  sbgoldbalt  48879  nnsum4primesevenALTV  48899  usgrexmpl2nb0  49129  usgrexmpl2nb3  49132  gpg3nbgrvtx0  49174  gpg3nbgrvtx0ALT  49175  gpg3nbgrvtx1  49176  gpg5grlim  49191  gpg5grlic  49192  0nodd  49267  oddinmgm  49272  2zrng0  49341  zlmodzxz0  49468  zlmodzxzequa  49608  zlmodzxzequap  49611  zlmodzxzldeplem3  49614  nnlog2ge0lt1  49678  blen1  49696  blen2  49697  nnolog2flm1  49702  ackval42  49808  ehl2eudisval0  49837  line2ylem  49863  i0oii  50028  io1ii  50029  sepfsepc  50036  rescofuf  50201  setc1ohomfval  50601  setc1ocofval  50602