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  33287  dp2clq  33489  dp2lt  33493  dp2ltc  33495  dpexpp1  33516  dpmul  33521  dpmul4  33522  elxrge02  33540  xrge0adddir  33621  psgnid  33700  cnmsgn0g  33749  altgnsg  33752  xrnarchi  33787  xrge0slmod  33951  znfermltl  33964  ccfldextdgrr  34346  cos9thpiminplylem4  34459  cos9thpiminplylem5  34460  raddcn  34603  xrge0iifcnv  34607  xrge0iifiso  34609  xrge0iifhmeo  34610  xrge0iifhom  34611  xrge0iifmhm  34613  xrge0mulc1cn  34615  lmlimxrge0  34622  pnfneige0  34625  lmxrge0  34626  zringnm  34632  rezh  34643  qqh0  34658  qqh1  34659  qqhucn  34666  esumpinfval  34747  hashf2  34758  esumcvg  34760  br2base  34943  sxbrsigalem3  34946  dya2iocbrsiga  34949  dya2icobrsiga  34950  sxbrsigalem1  34959  sxbrsigalem2  34960  sxbrsigalem4  34961  sxbrsigalem5  34962  sxbrsiga  34964  ballotlem2  35163  ballotlem4  35173  ballotlemi1  35177  ballotth  35212  signstf  35237  itgexpif  35277  chtvalz  35300  hgt750lemd  35319  hgt750lem  35322  tgoldbachgnn  35330  subfacp1lem1  35986  subfacp1lem6  35992  kur14lem6  36018  cvmliftlem4  36095  satf0suc  36183  problem4  36475  quad3  36477  iexpire  36542  fvtransport  36839  ttcid  37322  dfttc2g  37336  bj-minftyccb  38189  taupilem2  38286  iccioo01  38293  1oequni2o  38334  finxp1o  38358  finxpreclem4  38360  cos2h  38577  tan2h  38578  poimirlem9  38590  poimirlem27  38608  poimirlem28  38609  ismblfin  38622  mbfposadd  38628  ftc1anclem5  38658  asindmre  38664  dvasin  38665  dvacos  38666  rrnval  38804  dihjatcclem4  42521  lcmineqlem12  43133  fisdomnn  43338  subex  43341  absex  43342  cjex  43343  cxpi11d  43437  redvmptabs  43454  readvrec  43456  sn-00idlem2  43493  sn-00id  43495  remul02  43499  rabren3dioph  43864  jm2.27dlem2  44059  rmydioph  44063  rmxdioph  44065  expdiophlem2  44071  expdioph  44072  arearect  44259  areaquad  44260  2omomeqom  44347  omnord1ex  44348  corclrcl  44749  iunrelexpuztr  44761  corcltrcl  44781  dffrege76  44981  k0004val0  45196  lhe4.4ex1a  45355  binomcxplemdvbinom  45379  binomcxplemnotnn0  45382  ax6e2ndeqALT  45955  sineq0ALT  45961  nregmodelf1o  46047  pnfel0pnf  46582  lptioo2cn  46697  limsup10ex  46825  liminf10ex  46826  icccncfext  46939  itgsin0pilem1  47002  itgsbtaddcnst  47034  stoweidlem13  47065  wallispilem2  47118  wallispilem4  47120  wallispi2lem1  47123  stirlinglem13  47138  dirkerper  47148  dirkertrigeqlem3  47152  dirkeritg  47154  dirkercncflem1  47155  dirkercncflem4  47158  fourierdlem42  47201  fourierdlem62  47220  fourierdlem102  47260  fourierdlem103  47261  fourierdlem104  47262  fourierdlem114  47272  sqwvfoura  47280  fourierswlem  47282  fouriersw  47283  smfmullem4  47846  sqrtnnaa  47955  sqrtnzqaa  47956  goldpolyfactor  47969  goldracos5teq  47974  goldratmolem2  47975  goldratval  47978  sqrtnpoly  47985  ceil5half3  48458  8mod5e3  48478  fmtnoprmfac2lem1  48693  fmtno4prm  48702  3exp4mod41  48743  41prothprmlem2  48745  ppivalnn4  48754  6gbe  48911  7gbow  48912  8gbe  48913  9gbo  48914  11gbo  48915  sbgoldbalt  48921  nnsum4primesevenALTV  48941  usgrexmpl2nb0  49171  usgrexmpl2nb3  49174  gpg3nbgrvtx0  49216  gpg3nbgrvtx0ALT  49217  gpg3nbgrvtx1  49218  gpg5grlim  49233  gpg5grlic  49234  0nodd  49309  oddinmgm  49314  2zrng0  49383  zlmodzxz0  49510  zlmodzxzequa  49650  zlmodzxzequap  49653  zlmodzxzldeplem3  49656  nnlog2ge0lt1  49720  blen1  49738  blen2  49739  nnolog2flm1  49744  ackval42  49850  ehl2eudisval0  49879  line2ylem  49905  i0oii  50070  io1ii  50071  sepfsepc  50078  rescofuf  50243  setc1ohomfval  50643  setc1ocofval  50644