Theorem mp3an 1458

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  raltp  4601  rextp  4602  opthhausdorff  5372  funopg  6358  feq12i  6480  ftp  6896  caovass  7328  caovdi  7347  ordom  7569  mptexw  7636  ofmres  7667  mpoexw  7759  omopthlem1  8265  omopthlem2  8266  omopthi  8267  xpcomen  8591  unfilem3  8768  hartogs  8992  card2on  9002  unwf  9223  inlresf1  9328  inrresf1  9330  tskwe  9363  alephsmo  9513  dfac4  9533  dfac2a  9540  ackbij1lem13  9643  axdc2lem  9859  axcclem  9868  ondomon  9974  cfpwsdom  9995  pwfseqlem2  10070  pwfseqlem3  10071  1lt2pi  10316  addassi  10640  mulassi  10641  adddii  10642  adddiri  10643  lttri  10755  lelttri  10756  ltletri  10757  letri  10758  ltadd2i  10760  mul02lem2  10806  addid1  10809  addcani  10822  addcan2i  10823  mul12i  10824  mul32i  10825  add12i  10851  add32i  10852  subaddi  10962  subadd2i  10963  subsub23i  10965  addsubassi  10966  addsubi  10967  subcani  10968  subcan2i  10969  pnncani  10970  subdii  11078  subdiri  11079  ltadd1i  11183  leadd1i  11184  leadd2i  11185  ltsubaddi  11186  lesubaddi  11187  ltsubadd2i  11188  lesubadd2i  11189  ltaddsubi  11190  mulcani  11268  div23i  11387  div11i  11388  1mhlfehlf  11844  halfpm6th  11846  3halfnz  12049  addex  12375  mulex  12376  unirnioo  12827  ioorebas  12829  xnn0xrge0  12884  fldiv4lem1div2  13202  uzenom  13327  nnenom  13343  seqexw  13380  m1expcl2  13447  i4  13563  expnass  13566  faclbnd4lem1  13649  bcn1  13669  hashfxnn0  13693  ccat2s1p1  13976  ccat2s1p2  13977  cats1fvn  14211  cats1fv  14212  cats1cat  14214  cats2cat  14215  wrdlen3s3  14302  abs3difi  14761  0.999...  15229  bpoly3  15404  ef01bndlem  15529  cos1bnd  15532  cos2bnd  15533  sin4lt0  15540  rpnnen2lem3  15561  rpnnen2lem11  15569  rpnnen  15572  rexpen  15573  aleph1irr  15591  3dvdsdec  15673  3dvds2dec  15674  divalglem2  15736  ndvdsi  15753  flodddiv4  15754  gcdaddmlem  15862  bezout  15881  3lcm2e6woprm  15949  6lcm4e12  15950  lcmf0  15968  lcmf2a3a4e12  15981  dec2dvds  16389  modxai  16394  modsubi  16398  gcdi  16399  numexp2x  16405  2exp5  16412  prdsval  16720  0symgefmndeq  18514  pmtrprfval  18607  m1expaddsub  18618  0frgp  18897  staffval  19611  cnfldcj  20098  cnfldds  20101  cnfldfun  20103  xrsadd  20108  xrsmul  20109  xrsds  20134  cnmgpid  20153  nn0srg  20161  rge0srg  20162  zring0  20173  cnmsgnsubg  20266  psgninv  20271  re0g  20301  ocvfval  20355  frlmbas  20444  mdetrlin  21207  mdetunilem9  21225  leordtval2  21817  iscnp2  21844  utop3cls  22857  nmfval  23195  nmoffn  23317  nmofval  23320  icccld  23372  addcnlem  23469  iimulcn  23543  icopnfhmeo  23548  iccpnfcnv  23549  iccpnfhmeo  23550  xrhmeo  23551  xrhmph  23552  oprpiece1res1  23556  oprpiece1res2  23557  ishtpy  23577  pcoass  23629  cnstrcvs  23746  cncvs  23750  recvs  23751  qcvs  23752  zclmncvs  23753  tcphex  23821  cnfldcusp  23961  resscdrg  23962  reust  23985  recusp  23986  vitalilem4  24215  vitalilem5  24216  mbfdm  24230  dveflem  24582  dvlipcn  24597  c1lip2  24601  dgrid  24861  iaa  24921  abelthlem3  25028  abelthlem5  25030  abelth  25036  efcn  25038  sinhalfpilem  25056  sincosq1lem  25090  sincosq4sgn  25094  tangtx  25098  sincos4thpi  25106  sincos6thpi  25108  pigt3  25110  pige3ALT  25112  cos0pilt1  25124  relogcn  25229  dvlog2lem  25243  dvlog2  25244  logtayl  25251  logtayl2  25253  cxpsqrtlem  25293  cxpsqrt  25294  2irrexpq  25321  cxpcn2  25335  cxpcn3  25337  logblog  25378  2logb9irr  25381  2logb3irr  25383  2logb9irrALT  25384  sqrt2cxp2logb9e3  25385  2irrexpqALT  25386  ang180lem1  25395  ang180lem2  25396  1cubrlem  25427  mcubic  25433  quart1lem  25441  quart1  25442  reasinsin  25482  atancj  25496  efiatan  25498  atantan  25509  atanbndlem  25511  atan1  25514  atancn  25522  atantayl2  25524  log2cnv  25530  log2tlbnd  25531  log2ublem1  25532  log2ublem2  25533  log2ub  25535  efrlim  25555  scvxcvx  25571  1sgm2ppw  25784  ppiub  25788  bclbnd  25864  bposlem8  25875  lgsdir2lem1  25909  lgsdir2lem5  25913  lgseisenlem1  25959  lgseisenlem2  25960  lgsquadlem1  25964  chebbnd1  26056  dchrvmasumlem2  26082  istrkg3ld  26255  trgcgrg  26309  ax5seglem7  26729  axlowdimlem6  26741  axlowdimlem8  26743  axlowdimlem11  26746  elntg2  26779  cusgrsizeindb1  27240  vtxdginducedm1  27333  0grrusgr  27369  erclwwlktr  27807  erclwwlkntr  27856  wlk2v2e  27942  upgr3v3e3cycl  27965  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  konigsberglem5  28041  ex-fl  28232  ex-mod  28234  ex-hash  28238  ex-lcm  28243  0vfval  28389  smcnlem  28480  lnocoi  28540  nmlno0lem  28576  nmblolbii  28582  blocnilem  28587  blocni  28588  cncph  28602  isph  28605  ip0i  28608  ip1ilem  28609  ip2i  28611  ipdirilem  28612  ipasslem7  28619  ipasslem8  28620  ipasslem9  28621  ipasslem10  28622  ipasslem11  28623  ip2dii  28627  pythi  28633  siilem1  28634  siilem2  28635  siii  28636  hvmulassi  28829  hvmulcomi  28830  hvdistr1i  28834  hvsubdistr1i  28835  hvassi  28836  hvadd32i  28837  hvsubassi  28838  hvsub32i  28839  normlem0  28892  normlem8  28900  normlem9  28901  bcseqi  28903  polid2i  28940  hhph  28961  hlim0  29018  shscli  29100  shlessi  29160  shlej1i  29161  omlsilem  29185  shlubi  29198  h1de2i  29336  pjadjii  29457  pjaddii  29458  pjmulii  29460  pjdifnormii  29466  pjcji  29467  hoaddsubassi  29603  eigrei  29617  eigposi  29619  eigorthi  29620  adj0  29777  lnopeq0lem1  29788  lnopunilem1  29793  lnophmlem2  29800  nmcexi  29809  nmcopexi  29810  lnfn0i  29825  nmcfnexi  29834  mdexchi  30118  xppreima2  30413  dp2clq  30583  dp2lt  30587  dp2ltc  30589  dpexpp1  30610  dpmul  30615  dpmul4  30616  elxrge02  30634  xrge0adddir  30726  psgnid  30789  cnmsgn0g  30838  altgnsg  30841  xrnarchi  30863  xrge0slmod  30968  ccfldextdgrr  31145  raddcn  31282  xrge0iifcnv  31286  xrge0iifiso  31288  xrge0iifhmeo  31289  xrge0iifhom  31290  xrge0iifmhm  31292  xrge0mulc1cn  31294  lmlimxrge0  31301  pnfneige0  31304  lmxrge0  31305  zringnm  31311  rezh  31322  qqh0  31335  qqh1  31336  qqhucn  31343  esumpinfval  31442  hashf2  31453  esumcvg  31455  br2base  31637  sxbrsigalem3  31640  dya2iocbrsiga  31643  dya2icobrsiga  31644  sxbrsigalem1  31653  sxbrsigalem2  31654  sxbrsigalem4  31655  sxbrsigalem5  31656  sxbrsiga  31658  ballotlem2  31856  ballotlem4  31866  ballotlemi1  31870  ballotth  31905  sgnclre  31907  signstf  31946  itgexpif  31987  chtvalz  32010  hgt750lemd  32029  hgt750lem  32032  tgoldbachgnn  32040  lfuhgr2  32478  subfacp1lem1  32539  subfacp1lem6  32545  kur14lem6  32571  cvmliftlem4  32648  satf0suc  32736  problem4  33024  quad3  33026  logi  33079  iexpire  33080  fununiq  33125  fvtransport  33606  bj-minftyccb  34640  taupilem2  34736  iccioo01  34741  1oequni2o  34785  finxp1o  34809  finxpreclem4  34811  cos2h  35048  tan2h  35049  poimirlem9  35066  poimirlem27  35084  poimirlem28  35085  ismblfin  35098  mbfposadd  35104  ftc1anclem5  35134  asindmre  35140  dvasin  35141  dvacos  35142  rrnval  35265  el3v  35651  dihjatcclem4  38717  lcmineqlem12  39328  sn-00idlem2  39537  sn-00id  39539  remul02  39543  rei4  39560  sn-0lt1  39587  rabren3dioph  39756  jm2.27dlem2  39951  rmydioph  39955  rmxdioph  39957  expdiophlem2  39963  expdioph  39964  arearect  40165  areaquad  40166  corclrcl  40408  iunrelexpuztr  40420  corcltrcl  40440  dffrege76  40640  k0004val0  40857  lhe4.4ex1a  41033  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  ax6e2ndeqALT  41637  sineq0ALT  41643  pnfel0pnf  42165  lptioo2cn  42287  limsup10ex  42415  liminf10ex  42416  icccncfext  42529  itgsin0pilem1  42592  itgsbtaddcnst  42624  stoweidlem13  42655  wallispilem2  42708  wallispilem4  42710  wallispi2lem1  42713  stirlinglem13  42728  dirkerper  42738  dirkertrigeqlem3  42742  dirkeritg  42744  dirkercncflem1  42745  dirkercncflem4  42748  fourierdlem42  42791  fourierdlem62  42810  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem114  42862  sqwvfoura  42870  fourierswlem  42872  fouriersw  42873  smfmullem4  43426  fmtnoprmfac2lem1  44083  fmtno4prm  44092  2exp11  44118  3exp4mod41  44134  41prothprmlem2  44136  6gbe  44289  7gbow  44290  8gbe  44291  9gbo  44292  11gbo  44293  sbgoldbalt  44299  nnsum4primesevenALTV  44319  0nodd  44430  oddinmgm  44435  2zrng0  44562  zlmodzxz0  44758  zlmodzxzequa  44905  zlmodzxzequap  44908  zlmodzxzldeplem3  44911  nnlog2ge0lt1  44980  blen1  44998  blen2  44999  nnolog2flm1  45004  ackval42  45110  ehl2eudisval0  45139  line2ylem  45165