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 1085

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

This theorem is referenced by:  raltp  4710  rextp  4711  opthhausdorff  5519  funopg  6587  feq12i  6715  ftp  7166  caovass  7621  caovdi  7640  ordom  7880  mptexw  7956  ofmres  7988  sbcoteq1a  8055  mpoexw  8083  xpord3lem  8154  omopthlem1  8680  omopthlem2  8681  omopthi  8682  on2recsfn  8688  xpcomen  9088  snnen2o  9262  unfilem3  9337  hartogs  9568  card2on  9578  unwf  9834  inlresf1  9939  inrresf1  9941  tskwe  9974  alephsmo  10126  dfac4  10146  dfac2a  10153  ackbij1lem13  10256  axdc2lem  10472  axcclem  10481  ondomon  10587  cfpwsdom  10608  pwfseqlem2  10683  pwfseqlem3  10684  1lt2pi  10929  addassi  11255  mulassi  11256  adddii  11257  adddiri  11258  lttri  11371  lelttri  11372  ltletri  11373  letri  11374  ltadd2i  11376  mul02lem2  11422  addrid  11425  addcani  11438  addcan2i  11439  mul12i  11440  mul32i  11441  add12i  11467  add32i  11468  subaddi  11578  subadd2i  11579  subsub23i  11581  addsubassi  11582  addsubi  11583  subcani  11584  subcan2i  11585  pnncani  11586  subdii  11694  subdiri  11695  ltadd1i  11799  leadd1i  11800  leadd2i  11801  ltsubaddi  11802  lesubaddi  11803  ltsubadd2i  11804  lesubadd2i  11805  ltaddsubi  11806  mulcani  11884  div23i  12003  div11i  12004  1mhlfehlf  12462  halfpm6th  12464  3halfnz  12672  mpoaddex  13003  addex  13004  mpomulex  13005  mulex  13006  unirnioo  13459  ioorebas  13461  xnn0xrge0  13516  fldiv4lem1div2  13835  uzenom  13962  nnenom  13978  seqexw  14015  m1expcl2  14083  i4  14200  expnass  14204  faclbnd4lem1  14285  bcn1  14305  hashfxnn0  14329  ccat2s1p1  14612  ccat2s1p2  14613  cats1fvn  14842  cats1fv  14843  cats1cat  14845  cats2cat  14846  wrdlen3s3  14933  abs3difi  15389  0.999...  15860  bpoly3  16035  ef01bndlem  16161  cos1bnd  16164  cos2bnd  16165  sin4lt0  16172  rpnnen2lem3  16193  rpnnen2lem11  16201  rpnnen  16204  rexpen  16205  aleph1irr  16223  3dvdsdec  16309  3dvds2dec  16310  divalglem2  16372  ndvdsi  16389  flodddiv4  16390  gcdaddmlem  16499  bezout  16519  3lcm2e6woprm  16586  6lcm4e12  16587  lcmf0  16605  lcmf2a3a4e12  16618  dec2dvds  17032  modxai  17037  modsubi  17041  gcdi  17042  numexp2x  17048  2exp5  17055  2exp11  17059  0symgefmndeq  19348  pmtrprfval  19442  m1expaddsub  19453  0frgp  19734  staffval  20727  cnfldcj  21288  cnfldds  21291  cnfldfunALT  21294  cnfldcjOLD  21301  cnflddsOLD  21304  cnfldfunALTOLD  21307  cnfldfunALTOLDOLD  21308  xrsadd  21312  xrsmul  21313  xrsds  21342  cnmgpid  21362  nn0srg  21370  rge0srg  21371  zring0  21384  pzriprnglem13  21419  pzriprng1ALT  21422  fermltlchr  21459  cnmsgnsubg  21509  psgninv  21514  re0g  21544  ocvfval  21598  frlmbas  21689  mdetrlin  22517  mdetunilem9  22535  leordtval2  23129  iscnp2  23156  utop3cls  24169  nmfval  24510  nmoffn  24641  nmofval  24644  icccld  24696  addcnlem  24793  iimulcn  24874  iimulcnOLD  24875  icopnfhmeo  24881  iccpnfcnv  24882  iccpnfhmeo  24883  xrhmeo  24884  xrhmph  24885  oprpiece1res1  24889  oprpiece1res2  24890  ishtpy  24911  pcoass  24964  cnstrcvs  25081  cncvs  25085  recvs  25086  recvsOLD  25087  qcvs  25088  zclmncvs  25089  tcphex  25158  cnfldcusp  25298  resscdrg  25299  reust  25322  recusp  25323  vitalilem4  25553  vitalilem5  25554  mbfdm  25568  dveflem  25924  dvlipcn  25940  c1lip2  25944  dgrid  26212  iaa  26273  abelthlem3  26383  abelthlem5  26385  abelth  26391  efcn  26393  sinhalfpilem  26411  sincosq1lem  26445  sincosq4sgn  26449  tangtx  26453  sincos4thpi  26461  sincos6thpi  26463  pigt3  26465  pige3ALT  26467  cos0pilt1  26479  logi  26534  relogcn  26585  dvlog2lem  26599  dvlog2  26600  logtayl  26607  logtayl2  26609  cxpsqrtlem  26649  cxpsqrt  26650  2irrexpq  26678  cxpcn2  26694  cxpcn3  26696  logblog  26737  2logb9irr  26740  2logb3irr  26742  2logb9irrALT  26743  sqrt2cxp2logb9e3  26744  2irrexpqALT  26745  ang180lem1  26754  ang180lem2  26755  1cubrlem  26786  mcubic  26792  quart1lem  26800  quart1  26801  reasinsin  26841  atancj  26855  efiatan  26857  atantan  26868  atanbndlem  26870  atan1  26873  atancn  26881  atantayl2  26883  log2cnv  26889  log2tlbnd  26890  log2ublem1  26891  log2ublem2  26892  log2ub  26894  efrlim  26914  efrlimOLD  26915  scvxcvx  26931  1sgm2ppw  27146  ppiub  27150  bclbnd  27226  bposlem8  27237  lgsdir2lem1  27271  lgsdir2lem5  27275  lgseisenlem1  27321  lgseisenlem2  27322  lgsquadlem1  27326  chebbnd1  27418  dchrvmasumlem2  27444  norecfn  27876  norec2fn  27886  addsproplem2  27900  addsproplem6  27904  negsproplem2  27954  mulsproplem2  28030  mulsproplem3  28031  mulsproplem5  28033  mulsproplem6  28034  mulsproplem7  28035  mulsproplem8  28036  mulsproplem13  28041  mulsproplem14  28042  istrkg3ld  28278  trgcgrg  28332  ax5seglem7  28759  axlowdimlem6  28771  axlowdimlem8  28773  axlowdimlem11  28776  elntg2  28809  cusgrsizeindb1  29277  vtxdginducedm1  29370  0grrusgr  29406  erclwwlktr  29845  erclwwlkntr  29894  wlk2v2e  29980  upgr3v3e3cycl  30003  konigsberglem1  30075  konigsberglem2  30076  konigsberglem3  30077  konigsberglem5  30079  ex-fl  30270  ex-mod  30272  ex-hash  30276  ex-lcm  30281  0vfval  30429  smcnlem  30520  lnocoi  30580  nmlno0lem  30616  nmblolbii  30622  blocnilem  30627  blocni  30628  cncph  30642  isph  30645  ip0i  30648  ip1ilem  30649  ip2i  30651  ipdirilem  30652  ipasslem7  30659  ipasslem8  30660  ipasslem9  30661  ipasslem10  30662  ipasslem11  30663  ip2dii  30667  pythi  30673  siilem1  30674  siilem2  30675  siii  30676  hvmulassi  30869  hvmulcomi  30870  hvdistr1i  30874  hvsubdistr1i  30875  hvassi  30876  hvadd32i  30877  hvsubassi  30878  hvsub32i  30879  normlem0  30932  normlem8  30940  normlem9  30941  bcseqi  30943  polid2i  30980  hhph  31001  hlim0  31058  shscli  31140  shlessi  31200  shlej1i  31201  omlsilem  31225  shlubi  31238  h1de2i  31376  pjadjii  31497  pjaddii  31498  pjmulii  31500  pjdifnormii  31506  pjcji  31507  hoaddsubassi  31643  eigrei  31657  eigposi  31659  eigorthi  31660  adj0  31817  lnopeq0lem1  31828  lnopunilem1  31833  lnophmlem2  31840  nmcexi  31849  nmcopexi  31850  lnfn0i  31865  nmcfnexi  31874  mdexchi  32158  xppreima2  32450  dp2clq  32617  dp2lt  32621  dp2ltc  32623  dpexpp1  32644  dpmul  32649  dpmul4  32650  elxrge02  32668  xrge0adddir  32761  psgnid  32831  cnmsgn0g  32880  altgnsg  32883  xrnarchi  32905  xrge0slmod  33073  znfermltl  33091  ccfldextdgrr  33360  raddcn  33530  xrge0iifcnv  33534  xrge0iifiso  33536  xrge0iifhmeo  33537  xrge0iifhom  33538  xrge0iifmhm  33540  xrge0mulc1cn  33542  lmlimxrge0  33549  pnfneige0  33552  lmxrge0  33553  zringnm  33559  rezh  33572  qqh0  33585  qqh1  33586  qqhucn  33593  esumpinfval  33692  hashf2  33703  esumcvg  33705  br2base  33889  sxbrsigalem3  33892  dya2iocbrsiga  33895  dya2icobrsiga  33896  sxbrsigalem1  33905  sxbrsigalem2  33906  sxbrsigalem4  33907  sxbrsigalem5  33908  sxbrsiga  33910  ballotlem2  34108  ballotlem4  34118  ballotlemi1  34122  ballotth  34157  sgnclre  34159  signstf  34198  itgexpif  34238  chtvalz  34261  hgt750lemd  34280  hgt750lem  34283  tgoldbachgnn  34291  lfuhgr2  34728  subfacp1lem1  34789  subfacp1lem6  34795  kur14lem6  34821  cvmliftlem4  34898  satf0suc  34986  problem4  35272  quad3  35274  iexpire  35329  fununiq  35364  fvtransport  35628  bj-minftyccb  36704  taupilem2  36801  iccioo01  36806  1oequni2o  36847  finxp1o  36871  finxpreclem4  36873  cos2h  37084  tan2h  37085  poimirlem9  37102  poimirlem27  37120  poimirlem28  37121  ismblfin  37134  mbfposadd  37140  ftc1anclem5  37170  asindmre  37176  dvasin  37177  dvacos  37178  rrnval  37300  el3v  37691  dihjatcclem4  40894  lcmineqlem12  41511  cxpi11d  41914  sn-00idlem2  41954  sn-00id  41956  remul02  41960  rabren3dioph  42235  jm2.27dlem2  42431  rmydioph  42435  rmxdioph  42437  expdiophlem2  42443  expdioph  42444  arearect  42643  areaquad  42644  2omomeqom  42732  omnord1ex  42733  corclrcl  43137  iunrelexpuztr  43149  corcltrcl  43169  dffrege76  43369  k0004val0  43584  lhe4.4ex1a  43766  binomcxplemdvbinom  43790  binomcxplemnotnn0  43793  ax6e2ndeqALT  44370  sineq0ALT  44376  pnfel0pnf  44913  lptioo2cn  45033  limsup10ex  45161  liminf10ex  45162  icccncfext  45275  itgsin0pilem1  45338  itgsbtaddcnst  45370  stoweidlem13  45401  wallispilem2  45454  wallispilem4  45456  wallispi2lem1  45459  stirlinglem13  45474  dirkerper  45484  dirkertrigeqlem3  45488  dirkeritg  45490  dirkercncflem1  45491  dirkercncflem4  45494  fourierdlem42  45537  fourierdlem62  45556  fourierdlem102  45596  fourierdlem103  45597  fourierdlem104  45598  fourierdlem114  45608  sqwvfoura  45616  fourierswlem  45618  fouriersw  45619  smfmullem4  46182  fmtnoprmfac2lem1  46906  fmtno4prm  46915  3exp4mod41  46956  41prothprmlem2  46958  6gbe  47111  7gbow  47112  8gbe  47113  9gbo  47114  11gbo  47115  sbgoldbalt  47121  nnsum4primesevenALTV  47141  0nodd  47232  oddinmgm  47237  2zrng0  47306  zlmodzxz0  47420  zlmodzxzequa  47564  zlmodzxzequap  47567  zlmodzxzldeplem3  47570  nnlog2ge0lt1  47639  blen1  47657  blen2  47658  nnolog2flm1  47663  ackval42  47769  ehl2eudisval0  47798  line2ylem  47824  i0oii  47938  io1ii  47939  sepfsepc  47946