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  3438  raltp  4650  rextp  4651  opthhausdorff  5469  funopg  6530  feq12i  6659  ftp  7108  caovass  7564  caovdi  7583  ordom  7824  mptexw  7903  ofmres  7934  sbcoteq1a  8001  mpoexw  8028  xpord3lem  8096  omopthlem1  8592  omopthlem2  8593  omopthi  8594  on2recsfn  8600  xpcomen  9003  snnen2o  9152  unfilem3  9214  hartogs  9456  card2on  9466  unwf  9731  inlresf1  9836  inrresf1  9838  tskwe  9871  alephsmo  10021  dfac4  10041  dfac2a  10049  ackbij1lem13  10150  axdc2lem  10367  axcclem  10376  ondomon  10482  cfpwsdom  10504  pwfseqlem2  10579  pwfseqlem3  10580  1lt2pi  10825  addassi  11152  mulassi  11153  adddii  11154  adddiri  11155  lttri  11269  lelttri  11270  ltletri  11271  letri  11272  ltadd2i  11274  mul02lem2  11320  addrid  11323  addcani  11336  addcan2i  11337  mul12i  11338  mul32i  11339  add12i  11366  add32i  11367  subaddi  11478  subadd2i  11479  subsub23i  11481  addsubassi  11482  addsubi  11483  subcani  11484  subcan2i  11485  pnncani  11486  subdii  11596  subdiri  11597  ltadd1i  11701  leadd1i  11702  leadd2i  11703  ltsubaddi  11704  lesubaddi  11705  ltsubadd2i  11706  lesubadd2i  11707  ltaddsubi  11708  mulcani  11786  div23i  11910  div11i  11911  3halfnz  12605  mpoaddex  12935  addex  12936  mpomulex  12937  mulex  12938  unirnioo  13399  ioorebas  13401  xnn0xrge0  13456  fldiv4lem1div2  13793  uzenom  13923  nnenom  13939  seqexw  13976  m1expcl2  14044  i4  14163  expnass  14167  faclbnd4lem1  14252  bcn1  14272  hashfxnn0  14296  ccat2s1p1  14589  ccat2s1p2  14590  cats1fvn  14817  cats1fv  14818  cats1cat  14820  cats2cat  14821  wrdlen3s3  14908  abs3difi  15369  0.999...  15843  bpoly3  16020  ef01bndlem  16148  cos1bnd  16151  cos2bnd  16152  sin4lt0  16159  rpnnen2lem3  16180  rpnnen2lem11  16188  rpnnen  16191  rexpen  16192  aleph1irr  16210  3dvdsdec  16298  3dvds2dec  16299  divalglem2  16361  ndvdsi  16378  flodddiv4  16381  gcdaddmlem  16490  bezout  16509  3lcm2e6woprm  16581  6lcm4e12  16582  lcmf0  16600  lcmf2a3a4e12  16613  dec2dvds  17031  modxai  17036  modsubi  17040  gcdi  17041  numexp2x  17046  2exp5  17053  2exp11  17057  ex-chn2  18601  0symgefmndeq  19366  pmtrprfval  19459  m1expaddsub  19470  0frgp  19751  staffval  20815  cnfldcj  21358  cnfldds  21361  cnfldfunALT  21364  xrsadd  21367  xrsmul  21368  xrsds  21387  cnmgpid  21406  nn0srg  21414  rge0srg  21415  zring0  21435  pzriprnglem13  21470  pzriprng1ALT  21473  fermltlchr  21506  cnmsgnsubg  21554  psgninv  21559  re0g  21589  ocvfval  21643  frlmbas  21732  mdetrlin  22564  mdetunilem9  22582  leordtval2  23174  iscnp2  23201  utop3cls  24213  nmfval  24550  nmoffn  24673  nmofval  24676  icccld  24728  addcnlem  24827  iimulcn  24902  icopnfhmeo  24907  iccpnfcnv  24908  iccpnfhmeo  24909  xrhmeo  24910  xrhmph  24911  oprpiece1res1  24915  oprpiece1res2  24916  ishtpy  24936  pcoass  24988  cnstrcvs  25105  cncvs  25109  recvs  25110  qcvs  25111  zclmncvs  25112  tcphex  25181  cnfldcusp  25321  resscdrg  25322  reust  25345  recusp  25346  vitalilem4  25575  vitalilem5  25576  mbfdm  25590  dveflem  25943  dvlipcn  25958  c1lip2  25962  dgrid  26226  iaa  26288  abelthlem3  26395  abelthlem5  26397  abelth  26403  efcn  26405  sinhalfpilem  26424  sincosq1lem  26458  sincosq4sgn  26462  tangtx  26466  sincos4thpi  26474  sincos6thpi  26477  pigt3  26479  pige3ALT  26481  cos0pilt1  26493  logi  26548  relogcn  26599  dvlog2lem  26613  dvlog2  26614  logtayl  26621  logtayl2  26623  cxpsqrtlem  26663  cxpsqrt  26664  2irrexpq  26692  cxpcn2  26707  cxpcn3  26709  logblog  26753  2logb9irr  26756  2logb3irr  26758  2logb9irrALT  26759  sqrt2cxp2logb9e3  26760  2irrexpqALT  26761  ang180lem1  26770  ang180lem2  26771  1cubrlem  26802  mcubic  26808  quart1lem  26816  quart1  26817  reasinsin  26857  atancj  26871  efiatan  26873  atantan  26884  atanbndlem  26886  atan1  26889  atancn  26897  atantayl2  26899  log2cnv  26905  log2tlbnd  26906  log2ublem1  26907  log2ublem2  26908  log2ub  26910  efrlim  26930  scvxcvx  26946  1sgm2ppw  27160  ppiub  27164  bclbnd  27240  bposlem8  27251  lgsdir2lem1  27285  lgsdir2lem5  27289  lgseisenlem1  27335  lgseisenlem2  27336  lgsquadlem1  27340  chebbnd1  27432  dchrvmasumlem2  27458  norecfn  27935  norec2fn  27945  addsproplem2  27959  addsproplem6  27963  addbdaylem  28006  neg1s  28016  negsproplem2  28018  mulsproplem2  28106  mulsproplem3  28107  mulsproplem5  28109  mulsproplem6  28110  mulsproplem7  28111  mulsproplem8  28112  mulsproplem13  28117  mulsproplem14  28118  0zs  28377  zseo  28411  twocut  28412  bdaypw2n0bndlem  28452  bdaypw2bnd  28454  bdayfinbndlem1  28456  z12bdaylem2  28460  istrkg3ld  28526  trgcgrg  28580  ax5seglem7  29001  axlowdimlem6  29013  axlowdimlem8  29015  axlowdimlem11  29018  elntg2  29051  cusgrsizeindb1  29516  vtxdginducedm1  29609  0grrusgr  29645  erclwwlktr  30089  erclwwlkntr  30138  wlk2v2e  30224  upgr3v3e3cycl  30247  konigsberglem1  30319  konigsberglem2  30320  konigsberglem3  30321  konigsberglem5  30323  ex-fl  30514  ex-mod  30516  ex-hash  30520  ex-lcm  30525  0vfval  30674  smcnlem  30765  lnocoi  30825  nmlno0lem  30861  nmblolbii  30867  blocnilem  30872  blocni  30873  cncph  30887  isph  30890  ip0i  30893  ip1ilem  30894  ip2i  30896  ipdirilem  30897  ipasslem7  30904  ipasslem8  30905  ipasslem9  30906  ipasslem10  30907  ipasslem11  30908  ip2dii  30912  pythi  30918  siilem1  30919  siilem2  30920  siii  30921  hvmulassi  31114  hvmulcomi  31115  hvdistr1i  31119  hvsubdistr1i  31120  hvassi  31121  hvadd32i  31122  hvsubassi  31123  hvsub32i  31124  normlem0  31177  normlem8  31185  normlem9  31186  bcseqi  31188  polid2i  31225  hhph  31246  hlim0  31303  shscli  31385  shlessi  31445  shlej1i  31446  omlsilem  31470  shlubi  31483  h1de2i  31621  pjadjii  31742  pjaddii  31743  pjmulii  31745  pjdifnormii  31751  pjcji  31752  hoaddsubassi  31888  eigrei  31902  eigposi  31904  eigorthi  31905  adj0  32062  lnopeq0lem1  32073  lnopunilem1  32078  lnophmlem2  32085  nmcexi  32094  nmcopexi  32095  lnfn0i  32110  nmcfnexi  32119  mdexchi  32403  xppreima2  32721  sgnclre  32902  dp2clq  32937  dp2lt  32941  dp2ltc  32943  dpexpp1  32964  dpmul  32969  dpmul4  32970  elxrge02  32988  xrge0adddir  33075  psgnid  33155  cnmsgn0g  33204  altgnsg  33207  xrnarchi  33242  xrge0slmod  33405  znfermltl  33423  ccfldextdgrr  33813  cos9thpiminplylem4  33926  cos9thpiminplylem5  33927  raddcn  34070  xrge0iifcnv  34074  xrge0iifiso  34076  xrge0iifhmeo  34077  xrge0iifhom  34078  xrge0iifmhm  34080  xrge0mulc1cn  34082  lmlimxrge0  34089  pnfneige0  34092  lmxrge0  34093  zringnm  34099  rezh  34110  qqh0  34125  qqh1  34126  qqhucn  34133  esumpinfval  34214  hashf2  34225  esumcvg  34227  br2base  34410  sxbrsigalem3  34413  dya2iocbrsiga  34416  dya2icobrsiga  34417  sxbrsigalem1  34426  sxbrsigalem2  34427  sxbrsigalem4  34428  sxbrsigalem5  34429  sxbrsiga  34431  ballotlem2  34630  ballotlem4  34640  ballotlemi1  34644  ballotth  34679  signstf  34707  itgexpif  34747  chtvalz  34770  hgt750lemd  34789  hgt750lem  34792  tgoldbachgnn  34800  lfuhgr2  35298  subfacp1lem1  35358  subfacp1lem6  35364  kur14lem6  35390  cvmliftlem4  35467  satf0suc  35555  problem4  35847  quad3  35849  iexpire  35914  fununiq  35948  fvtransport  36211  ttcid  36671  dfttc2g  36685  bj-minftyccb  37536  taupilem2  37633  iccioo01  37640  1oequni2o  37681  finxp1o  37705  finxpreclem4  37707  cos2h  37929  tan2h  37930  poimirlem9  37947  poimirlem27  37965  poimirlem28  37966  ismblfin  37979  mbfposadd  37985  ftc1anclem5  38015  asindmre  38021  dvasin  38022  dvacos  38023  rrnval  38145  dihjatcclem4  41864  lcmineqlem12  42476  fisdomnn  42680  subex  42683  absex  42684  cjex  42685  cxpi11d  42772  redvmptabs  42789  readvrec  42791  sn-00idlem2  42828  sn-00id  42830  remul02  42834  rabren3dioph  43240  jm2.27dlem2  43435  rmydioph  43439  rmxdioph  43441  expdiophlem2  43447  expdioph  43448  arearect  43640  areaquad  43641  2omomeqom  43728  omnord1ex  43729  corclrcl  44131  iunrelexpuztr  44143  corcltrcl  44163  dffrege76  44363  k0004val0  44578  lhe4.4ex1a  44753  binomcxplemdvbinom  44777  binomcxplemnotnn0  44780  ax6e2ndeqALT  45354  sineq0ALT  45360  nregmodelf1o  45439  pnfel0pnf  45955  lptioo2cn  46070  limsup10ex  46198  liminf10ex  46199  icccncfext  46312  itgsin0pilem1  46375  itgsbtaddcnst  46407  stoweidlem13  46438  wallispilem2  46491  wallispilem4  46493  wallispi2lem1  46496  stirlinglem13  46511  dirkerper  46521  dirkertrigeqlem3  46525  dirkeritg  46527  dirkercncflem1  46528  dirkercncflem4  46531  fourierdlem42  46574  fourierdlem62  46593  fourierdlem102  46633  fourierdlem103  46634  fourierdlem104  46635  fourierdlem114  46645  sqwvfoura  46653  fourierswlem  46655  fouriersw  46656  smfmullem4  47219  nthrucw  47311  ceil5half3  47785  8mod5e3  47805  fmtnoprmfac2lem1  48020  fmtno4prm  48029  3exp4mod41  48070  41prothprmlem2  48072  ppivalnn4  48081  6gbe  48238  7gbow  48239  8gbe  48240  9gbo  48241  11gbo  48242  sbgoldbalt  48248  nnsum4primesevenALTV  48268  usgrexmpl2nb0  48498  usgrexmpl2nb3  48501  gpg3nbgrvtx0  48543  gpg3nbgrvtx0ALT  48544  gpg3nbgrvtx1  48545  gpg5grlim  48560  gpg5grlic  48561  0nodd  48637  oddinmgm  48642  2zrng0  48711  zlmodzxz0  48823  zlmodzxzequa  48963  zlmodzxzequap  48966  zlmodzxzldeplem3  48969  nnlog2ge0lt1  49033  blen1  49051  blen2  49052  nnolog2flm1  49057  ackval42  49163  ehl2eudisval0  49192  line2ylem  49218  i0oii  49386  io1ii  49387  sepfsepc  49394  rescofuf  49559  setc1ohomfval  49959  setc1ocofval  49960