Theorem mp3an 1464

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  el3v  3450  raltp  4664  rextp  4665  opthhausdorff  5475  funopg  6536  feq12i  6665  ftp  7114  caovass  7570  caovdi  7589  ordom  7830  mptexw  7909  ofmres  7940  sbcoteq1a  8007  mpoexw  8034  xpord3lem  8103  omopthlem1  8599  omopthlem2  8600  omopthi  8601  on2recsfn  8607  xpcomen  9010  snnen2o  9159  unfilem3  9221  hartogs  9463  card2on  9473  unwf  9736  inlresf1  9841  inrresf1  9843  tskwe  9876  alephsmo  10026  dfac4  10046  dfac2a  10054  ackbij1lem13  10155  axdc2lem  10372  axcclem  10381  ondomon  10487  cfpwsdom  10509  pwfseqlem2  10584  pwfseqlem3  10585  1lt2pi  10830  addassi  11156  mulassi  11157  adddii  11158  adddiri  11159  lttri  11273  lelttri  11274  ltletri  11275  letri  11276  ltadd2i  11278  mul02lem2  11324  addrid  11327  addcani  11340  addcan2i  11341  mul12i  11342  mul32i  11343  add12i  11370  add32i  11371  subaddi  11482  subadd2i  11483  subsub23i  11485  addsubassi  11486  addsubi  11487  subcani  11488  subcan2i  11489  pnncani  11490  subdii  11600  subdiri  11601  ltadd1i  11705  leadd1i  11706  leadd2i  11707  ltsubaddi  11708  lesubaddi  11709  ltsubadd2i  11710  lesubadd2i  11711  ltaddsubi  11712  mulcani  11790  div23i  11913  div11i  11914  3halfnz  12585  mpoaddex  12915  addex  12916  mpomulex  12917  mulex  12918  unirnioo  13379  ioorebas  13381  xnn0xrge0  13436  fldiv4lem1div2  13771  uzenom  13901  nnenom  13917  seqexw  13954  m1expcl2  14022  i4  14141  expnass  14145  faclbnd4lem1  14230  bcn1  14250  hashfxnn0  14274  ccat2s1p1  14567  ccat2s1p2  14568  cats1fvn  14795  cats1fv  14796  cats1cat  14798  cats2cat  14799  wrdlen3s3  14886  abs3difi  15347  0.999...  15818  bpoly3  15995  ef01bndlem  16123  cos1bnd  16126  cos2bnd  16127  sin4lt0  16134  rpnnen2lem3  16155  rpnnen2lem11  16163  rpnnen  16166  rexpen  16167  aleph1irr  16185  3dvdsdec  16273  3dvds2dec  16274  divalglem2  16336  ndvdsi  16353  flodddiv4  16356  gcdaddmlem  16465  bezout  16484  3lcm2e6woprm  16556  6lcm4e12  16557  lcmf0  16575  lcmf2a3a4e12  16588  dec2dvds  17005  modxai  17010  modsubi  17014  gcdi  17015  numexp2x  17020  2exp5  17027  2exp11  17031  ex-chn2  18575  0symgefmndeq  19340  pmtrprfval  19433  m1expaddsub  19444  0frgp  19725  staffval  20791  cnfldcj  21335  cnfldds  21338  cnfldfunALT  21341  cnfldcjOLD  21348  cnflddsOLD  21351  cnfldfunALTOLD  21354  xrsadd  21357  xrsmul  21358  xrsds  21381  cnmgpid  21401  nn0srg  21409  rge0srg  21410  zring0  21430  pzriprnglem13  21465  pzriprng1ALT  21468  fermltlchr  21501  cnmsgnsubg  21549  psgninv  21554  re0g  21584  ocvfval  21638  frlmbas  21727  mdetrlin  22563  mdetunilem9  22581  leordtval2  23173  iscnp2  23200  utop3cls  24212  nmfval  24549  nmoffn  24672  nmofval  24675  icccld  24727  addcnlem  24826  iimulcn  24907  iimulcnOLD  24908  icopnfhmeo  24914  iccpnfcnv  24915  iccpnfhmeo  24916  xrhmeo  24917  xrhmph  24918  oprpiece1res1  24922  oprpiece1res2  24923  ishtpy  24944  pcoass  24997  cnstrcvs  25114  cncvs  25118  recvs  25119  qcvs  25120  zclmncvs  25121  tcphex  25190  cnfldcusp  25330  resscdrg  25331  reust  25354  recusp  25355  vitalilem4  25585  vitalilem5  25586  mbfdm  25600  dveflem  25956  dvlipcn  25972  c1lip2  25976  dgrid  26243  iaa  26306  abelthlem3  26416  abelthlem5  26418  abelth  26424  efcn  26426  sinhalfpilem  26445  sincosq1lem  26479  sincosq4sgn  26483  tangtx  26487  sincos4thpi  26495  sincos6thpi  26498  pigt3  26500  pige3ALT  26502  cos0pilt1  26514  logi  26569  relogcn  26620  dvlog2lem  26634  dvlog2  26635  logtayl  26642  logtayl2  26644  cxpsqrtlem  26684  cxpsqrt  26685  2irrexpq  26713  cxpcn2  26729  cxpcn3  26731  logblog  26775  2logb9irr  26778  2logb3irr  26780  2logb9irrALT  26781  sqrt2cxp2logb9e3  26782  2irrexpqALT  26783  ang180lem1  26792  ang180lem2  26793  1cubrlem  26824  mcubic  26830  quart1lem  26838  quart1  26839  reasinsin  26879  atancj  26893  efiatan  26895  atantan  26906  atanbndlem  26908  atan1  26911  atancn  26919  atantayl2  26921  log2cnv  26927  log2tlbnd  26928  log2ublem1  26929  log2ublem2  26930  log2ub  26932  efrlim  26952  efrlimOLD  26953  scvxcvx  26969  1sgm2ppw  27184  ppiub  27188  bclbnd  27264  bposlem8  27275  lgsdir2lem1  27309  lgsdir2lem5  27313  lgseisenlem1  27359  lgseisenlem2  27360  lgsquadlem1  27364  chebbnd1  27456  dchrvmasumlem2  27482  norecfn  27959  norec2fn  27969  addsproplem2  27983  addsproplem6  27987  addbdaylem  28030  neg1s  28040  negsproplem2  28042  mulsproplem2  28130  mulsproplem3  28131  mulsproplem5  28133  mulsproplem6  28134  mulsproplem7  28135  mulsproplem8  28136  mulsproplem13  28141  mulsproplem14  28142  0zs  28401  zseo  28435  twocut  28436  bdaypw2n0bndlem  28476  bdaypw2bnd  28478  bdayfinbndlem1  28480  z12bdaylem2  28484  istrkg3ld  28551  trgcgrg  28605  ax5seglem7  29026  axlowdimlem6  29038  axlowdimlem8  29040  axlowdimlem11  29043  elntg2  29076  cusgrsizeindb1  29542  vtxdginducedm1  29635  0grrusgr  29671  erclwwlktr  30115  erclwwlkntr  30164  wlk2v2e  30250  upgr3v3e3cycl  30273  konigsberglem1  30345  konigsberglem2  30346  konigsberglem3  30347  konigsberglem5  30349  ex-fl  30540  ex-mod  30542  ex-hash  30546  ex-lcm  30551  0vfval  30700  smcnlem  30791  lnocoi  30851  nmlno0lem  30887  nmblolbii  30893  blocnilem  30898  blocni  30899  cncph  30913  isph  30916  ip0i  30919  ip1ilem  30920  ip2i  30922  ipdirilem  30923  ipasslem7  30930  ipasslem8  30931  ipasslem9  30932  ipasslem10  30933  ipasslem11  30934  ip2dii  30938  pythi  30944  siilem1  30945  siilem2  30946  siii  30947  hvmulassi  31140  hvmulcomi  31141  hvdistr1i  31145  hvsubdistr1i  31146  hvassi  31147  hvadd32i  31148  hvsubassi  31149  hvsub32i  31150  normlem0  31203  normlem8  31211  normlem9  31212  bcseqi  31214  polid2i  31251  hhph  31272  hlim0  31329  shscli  31411  shlessi  31471  shlej1i  31472  omlsilem  31496  shlubi  31509  h1de2i  31647  pjadjii  31768  pjaddii  31769  pjmulii  31771  pjdifnormii  31777  pjcji  31778  hoaddsubassi  31914  eigrei  31928  eigposi  31930  eigorthi  31931  adj0  32088  lnopeq0lem1  32099  lnopunilem1  32104  lnophmlem2  32111  nmcexi  32120  nmcopexi  32121  lnfn0i  32136  nmcfnexi  32145  mdexchi  32429  xppreima2  32747  sgnclre  32930  dp2clq  32979  dp2lt  32983  dp2ltc  32985  dpexpp1  33006  dpmul  33011  dpmul4  33012  elxrge02  33030  xrge0adddir  33117  psgnid  33197  cnmsgn0g  33246  altgnsg  33249  xrnarchi  33284  xrge0slmod  33447  znfermltl  33465  ccfldextdgrr  33856  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  raddcn  34113  xrge0iifcnv  34117  xrge0iifiso  34119  xrge0iifhmeo  34120  xrge0iifhom  34121  xrge0iifmhm  34123  xrge0mulc1cn  34125  lmlimxrge0  34132  pnfneige0  34135  lmxrge0  34136  zringnm  34142  rezh  34153  qqh0  34168  qqh1  34169  qqhucn  34176  esumpinfval  34257  hashf2  34268  esumcvg  34270  br2base  34453  sxbrsigalem3  34456  dya2iocbrsiga  34459  dya2icobrsiga  34460  sxbrsigalem1  34469  sxbrsigalem2  34470  sxbrsigalem4  34471  sxbrsigalem5  34472  sxbrsiga  34474  ballotlem2  34673  ballotlem4  34683  ballotlemi1  34687  ballotth  34722  signstf  34750  itgexpif  34790  chtvalz  34813  hgt750lemd  34832  hgt750lem  34835  tgoldbachgnn  34843  lfuhgr2  35341  subfacp1lem1  35401  subfacp1lem6  35407  kur14lem6  35433  cvmliftlem4  35510  satf0suc  35598  problem4  35890  quad3  35892  iexpire  35957  fununiq  35991  fvtransport  36254  bj-minftyccb  37507  taupilem2  37604  iccioo01  37609  1oequni2o  37650  finxp1o  37674  finxpreclem4  37676  cos2h  37891  tan2h  37892  poimirlem9  37909  poimirlem27  37927  poimirlem28  37928  ismblfin  37941  mbfposadd  37947  ftc1anclem5  37977  asindmre  37983  dvasin  37984  dvacos  37985  rrnval  38107  dihjatcclem4  41826  lcmineqlem12  42439  fisdomnn  42643  subex  42646  absex  42647  cjex  42648  cxpi11d  42742  redvmptabs  42759  readvrec  42761  sn-00idlem2  42798  sn-00id  42800  remul02  42804  rabren3dioph  43201  jm2.27dlem2  43396  rmydioph  43400  rmxdioph  43402  expdiophlem2  43408  expdioph  43409  arearect  43601  areaquad  43602  2omomeqom  43689  omnord1ex  43690  corclrcl  44092  iunrelexpuztr  44104  corcltrcl  44124  dffrege76  44324  k0004val0  44539  lhe4.4ex1a  44714  binomcxplemdvbinom  44738  binomcxplemnotnn0  44741  ax6e2ndeqALT  45315  sineq0ALT  45321  nregmodelf1o  45400  pnfel0pnf  45917  lptioo2cn  46032  limsup10ex  46160  liminf10ex  46161  icccncfext  46274  itgsin0pilem1  46337  itgsbtaddcnst  46369  stoweidlem13  46400  wallispilem2  46453  wallispilem4  46455  wallispi2lem1  46458  stirlinglem13  46473  dirkerper  46483  dirkertrigeqlem3  46487  dirkeritg  46489  dirkercncflem1  46490  dirkercncflem4  46493  fourierdlem42  46536  fourierdlem62  46555  fourierdlem102  46595  fourierdlem103  46596  fourierdlem104  46597  fourierdlem114  46607  sqwvfoura  46615  fourierswlem  46617  fouriersw  46618  smfmullem4  47181  nthrucw  47273  ceil5half3  47729  8mod5e3  47749  fmtnoprmfac2lem1  47955  fmtno4prm  47964  3exp4mod41  48005  41prothprmlem2  48007  6gbe  48160  7gbow  48161  8gbe  48162  9gbo  48163  11gbo  48164  sbgoldbalt  48170  nnsum4primesevenALTV  48190  usgrexmpl2nb0  48420  usgrexmpl2nb3  48423  gpg3nbgrvtx0  48465  gpg3nbgrvtx0ALT  48466  gpg3nbgrvtx1  48467  gpg5grlim  48482  gpg5grlic  48483  0nodd  48559  oddinmgm  48564  2zrng0  48633  zlmodzxz0  48745  zlmodzxzequa  48885  zlmodzxzequap  48888  zlmodzxzldeplem3  48891  nnlog2ge0lt1  48955  blen1  48973  blen2  48974  nnolog2flm1  48979  ackval42  49085  ehl2eudisval0  49114  line2ylem  49140  i0oii  49308  io1ii  49309  sepfsepc  49316  rescofuf  49481  setc1ohomfval  49881  setc1ocofval  49882