Theorem mp3an 1462

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  raltp  4709  rextp  4710  opthhausdorff  5517  funopg  6580  feq12i  6708  ftp  7152  caovass  7604  caovdi  7623  ordom  7862  mptexw  7936  ofmres  7968  sbcoteq1a  8034  mpoexw  8062  xpord3lem  8132  omopthlem1  8655  omopthlem2  8656  omopthi  8657  on2recsfn  8663  xpcomen  9060  snnen2o  9234  unfilem3  9309  hartogs  9536  card2on  9546  unwf  9802  inlresf1  9907  inrresf1  9909  tskwe  9942  alephsmo  10094  dfac4  10114  dfac2a  10121  ackbij1lem13  10224  axdc2lem  10440  axcclem  10449  ondomon  10555  cfpwsdom  10576  pwfseqlem2  10651  pwfseqlem3  10652  1lt2pi  10897  addassi  11221  mulassi  11222  adddii  11223  adddiri  11224  lttri  11337  lelttri  11338  ltletri  11339  letri  11340  ltadd2i  11342  mul02lem2  11388  addrid  11391  addcani  11404  addcan2i  11405  mul12i  11406  mul32i  11407  add12i  11433  add32i  11434  subaddi  11544  subadd2i  11545  subsub23i  11547  addsubassi  11548  addsubi  11549  subcani  11550  subcan2i  11551  pnncani  11552  subdii  11660  subdiri  11661  ltadd1i  11765  leadd1i  11766  leadd2i  11767  ltsubaddi  11768  lesubaddi  11769  ltsubadd2i  11770  lesubadd2i  11771  ltaddsubi  11772  mulcani  11850  div23i  11969  div11i  11970  1mhlfehlf  12428  halfpm6th  12430  3halfnz  12638  addex  12969  mulex  12970  unirnioo  13423  ioorebas  13425  xnn0xrge0  13480  fldiv4lem1div2  13799  uzenom  13926  nnenom  13942  seqexw  13979  m1expcl2  14048  i4  14165  expnass  14169  faclbnd4lem1  14250  bcn1  14270  hashfxnn0  14294  ccat2s1p1  14576  ccat2s1p2  14577  cats1fvn  14806  cats1fv  14807  cats1cat  14809  cats2cat  14810  wrdlen3s3  14897  abs3difi  15353  0.999...  15824  bpoly3  15999  ef01bndlem  16124  cos1bnd  16127  cos2bnd  16128  sin4lt0  16135  rpnnen2lem3  16156  rpnnen2lem11  16164  rpnnen  16167  rexpen  16168  aleph1irr  16186  3dvdsdec  16272  3dvds2dec  16273  divalglem2  16335  ndvdsi  16352  flodddiv4  16353  gcdaddmlem  16462  bezout  16482  3lcm2e6woprm  16549  6lcm4e12  16550  lcmf0  16568  lcmf2a3a4e12  16581  dec2dvds  16993  modxai  16998  modsubi  17002  gcdi  17003  numexp2x  17009  2exp5  17016  2exp11  17020  0symgefmndeq  19256  pmtrprfval  19350  m1expaddsub  19361  0frgp  19642  staffval  20448  cnfldcj  20944  cnfldds  20947  cnfldfunALT  20950  cnfldfunALTOLD  20951  xrsadd  20955  xrsmul  20956  xrsds  20981  cnmgpid  21000  nn0srg  21008  rge0srg  21009  zring0  21020  cnmsgnsubg  21122  psgninv  21127  re0g  21157  ocvfval  21211  frlmbas  21302  mdetrlin  22096  mdetunilem9  22114  leordtval2  22708  iscnp2  22735  utop3cls  23748  nmfval  24089  nmoffn  24220  nmofval  24223  icccld  24275  addcnlem  24372  iimulcn  24446  icopnfhmeo  24451  iccpnfcnv  24452  iccpnfhmeo  24453  xrhmeo  24454  xrhmph  24455  oprpiece1res1  24459  oprpiece1res2  24460  ishtpy  24480  pcoass  24532  cnstrcvs  24649  cncvs  24653  recvs  24654  recvsOLD  24655  qcvs  24656  zclmncvs  24657  tcphex  24726  cnfldcusp  24866  resscdrg  24867  reust  24890  recusp  24891  vitalilem4  25120  vitalilem5  25121  mbfdm  25135  dveflem  25488  dvlipcn  25503  c1lip2  25507  dgrid  25770  iaa  25830  abelthlem3  25937  abelthlem5  25939  abelth  25945  efcn  25947  sinhalfpilem  25965  sincosq1lem  25999  sincosq4sgn  26003  tangtx  26007  sincos4thpi  26015  sincos6thpi  26017  pigt3  26019  pige3ALT  26021  cos0pilt1  26033  relogcn  26138  dvlog2lem  26152  dvlog2  26153  logtayl  26160  logtayl2  26162  cxpsqrtlem  26202  cxpsqrt  26203  2irrexpq  26230  cxpcn2  26244  cxpcn3  26246  logblog  26287  2logb9irr  26290  2logb3irr  26292  2logb9irrALT  26293  sqrt2cxp2logb9e3  26294  2irrexpqALT  26295  ang180lem1  26304  ang180lem2  26305  1cubrlem  26336  mcubic  26342  quart1lem  26350  quart1  26351  reasinsin  26391  atancj  26405  efiatan  26407  atantan  26418  atanbndlem  26420  atan1  26423  atancn  26431  atantayl2  26433  log2cnv  26439  log2tlbnd  26440  log2ublem1  26441  log2ublem2  26442  log2ub  26444  efrlim  26464  scvxcvx  26480  1sgm2ppw  26693  ppiub  26697  bclbnd  26773  bposlem8  26784  lgsdir2lem1  26818  lgsdir2lem5  26822  lgseisenlem1  26868  lgseisenlem2  26869  lgsquadlem1  26873  chebbnd1  26965  dchrvmasumlem2  26991  norecfn  27420  norec2fn  27430  addsproplem2  27444  addsproplem6  27448  negsproplem2  27493  mulsproplem2  27563  mulsproplem3  27564  mulsproplem5  27566  mulsproplem6  27567  mulsproplem7  27568  mulsproplem8  27569  mulsproplem13  27574  mulsproplem14  27575  istrkg3ld  27702  trgcgrg  27756  ax5seglem7  28183  axlowdimlem6  28195  axlowdimlem8  28197  axlowdimlem11  28200  elntg2  28233  cusgrsizeindb1  28697  vtxdginducedm1  28790  0grrusgr  28826  erclwwlktr  29265  erclwwlkntr  29314  wlk2v2e  29400  upgr3v3e3cycl  29423  konigsberglem1  29495  konigsberglem2  29496  konigsberglem3  29497  konigsberglem5  29499  ex-fl  29690  ex-mod  29692  ex-hash  29696  ex-lcm  29701  0vfval  29847  smcnlem  29938  lnocoi  29998  nmlno0lem  30034  nmblolbii  30040  blocnilem  30045  blocni  30046  cncph  30060  isph  30063  ip0i  30066  ip1ilem  30067  ip2i  30069  ipdirilem  30070  ipasslem7  30077  ipasslem8  30078  ipasslem9  30079  ipasslem10  30080  ipasslem11  30081  ip2dii  30085  pythi  30091  siilem1  30092  siilem2  30093  siii  30094  hvmulassi  30287  hvmulcomi  30288  hvdistr1i  30292  hvsubdistr1i  30293  hvassi  30294  hvadd32i  30295  hvsubassi  30296  hvsub32i  30297  normlem0  30350  normlem8  30358  normlem9  30359  bcseqi  30361  polid2i  30398  hhph  30419  hlim0  30476  shscli  30558  shlessi  30618  shlej1i  30619  omlsilem  30643  shlubi  30656  h1de2i  30794  pjadjii  30915  pjaddii  30916  pjmulii  30918  pjdifnormii  30924  pjcji  30925  hoaddsubassi  31061  eigrei  31075  eigposi  31077  eigorthi  31078  adj0  31235  lnopeq0lem1  31246  lnopunilem1  31251  lnophmlem2  31258  nmcexi  31267  nmcopexi  31268  lnfn0i  31283  nmcfnexi  31292  mdexchi  31576  xppreima2  31864  dp2clq  32035  dp2lt  32039  dp2ltc  32041  dpexpp1  32062  dpmul  32067  dpmul4  32068  elxrge02  32086  xrge0adddir  32181  psgnid  32244  cnmsgn0g  32293  altgnsg  32296  xrnarchi  32318  xrge0slmod  32452  fermltlchr  32467  znfermltl  32468  ccfldextdgrr  32735  raddcn  32898  xrge0iifcnv  32902  xrge0iifiso  32904  xrge0iifhmeo  32905  xrge0iifhom  32906  xrge0iifmhm  32908  xrge0mulc1cn  32910  lmlimxrge0  32917  pnfneige0  32920  lmxrge0  32921  zringnm  32927  rezh  32940  qqh0  32953  qqh1  32954  qqhucn  32961  esumpinfval  33060  hashf2  33071  esumcvg  33073  br2base  33257  sxbrsigalem3  33260  dya2iocbrsiga  33263  dya2icobrsiga  33264  sxbrsigalem1  33273  sxbrsigalem2  33274  sxbrsigalem4  33275  sxbrsigalem5  33276  sxbrsiga  33278  ballotlem2  33476  ballotlem4  33486  ballotlemi1  33490  ballotth  33525  sgnclre  33527  signstf  33566  itgexpif  33607  chtvalz  33630  hgt750lemd  33649  hgt750lem  33652  tgoldbachgnn  33660  lfuhgr2  34098  subfacp1lem1  34159  subfacp1lem6  34165  kur14lem6  34191  cvmliftlem4  34268  satf0suc  34356  problem4  34642  quad3  34644  logi  34693  iexpire  34694  fununiq  34729  fvtransport  34993  gg-iimulcn  35158  bj-minftyccb  36095  taupilem2  36192  iccioo01  36197  1oequni2o  36238  finxp1o  36262  finxpreclem4  36264  cos2h  36468  tan2h  36469  poimirlem9  36486  poimirlem27  36504  poimirlem28  36505  ismblfin  36518  mbfposadd  36524  ftc1anclem5  36554  asindmre  36560  dvasin  36561  dvacos  36562  rrnval  36684  el3v  37075  dihjatcclem4  40281  lcmineqlem12  40894  sn-00idlem2  41269  sn-00id  41271  remul02  41275  rabren3dioph  41539  jm2.27dlem2  41735  rmydioph  41739  rmxdioph  41741  expdiophlem2  41747  expdioph  41748  arearect  41950  areaquad  41951  2omomeqom  42039  omnord1ex  42040  corclrcl  42444  iunrelexpuztr  42456  corcltrcl  42476  dffrege76  42676  k0004val0  42891  lhe4.4ex1a  43074  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  ax6e2ndeqALT  43678  sineq0ALT  43684  pnfel0pnf  44228  lptioo2cn  44348  limsup10ex  44476  liminf10ex  44477  icccncfext  44590  itgsin0pilem1  44653  itgsbtaddcnst  44685  stoweidlem13  44716  wallispilem2  44769  wallispilem4  44771  wallispi2lem1  44774  stirlinglem13  44789  dirkerper  44799  dirkertrigeqlem3  44803  dirkeritg  44805  dirkercncflem1  44806  dirkercncflem4  44809  fourierdlem42  44852  fourierdlem62  44871  fourierdlem102  44911  fourierdlem103  44912  fourierdlem104  44913  fourierdlem114  44923  sqwvfoura  44931  fourierswlem  44933  fouriersw  44934  smfmullem4  45497  fmtnoprmfac2lem1  46221  fmtno4prm  46230  3exp4mod41  46271  41prothprmlem2  46273  6gbe  46426  7gbow  46427  8gbe  46428  9gbo  46429  11gbo  46430  sbgoldbalt  46436  nnsum4primesevenALTV  46456  0nodd  46567  oddinmgm  46572  2zrng0  46790  zlmodzxz0  46986  zlmodzxzequa  47131  zlmodzxzequap  47134  zlmodzxzldeplem3  47137  nnlog2ge0lt1  47206  blen1  47224  blen2  47225  nnolog2flm1  47230  ackval42  47336  ehl2eudisval0  47365  line2ylem  47391  i0oii  47506  io1ii  47507  sepfsepc  47514