Theorem mp3an 1459

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 1446	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 688	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  4638  rextp  4639  opthhausdorff  5425  funopg  6452  feq12i  6577  ftp  7011  caovass  7450  caovdi  7469  ordom  7697  mptexw  7769  ofmres  7800  mpoexw  7892  omopthlem1  8449  omopthlem2  8450  omopthi  8451  xpcomen  8803  unfilem3  9010  hartogs  9233  card2on  9243  unwf  9499  inlresf1  9604  inrresf1  9606  tskwe  9639  alephsmo  9789  dfac4  9809  dfac2a  9816  ackbij1lem13  9919  axdc2lem  10135  axcclem  10144  ondomon  10250  cfpwsdom  10271  pwfseqlem2  10346  pwfseqlem3  10347  1lt2pi  10592  addassi  10916  mulassi  10917  adddii  10918  adddiri  10919  lttri  11031  lelttri  11032  ltletri  11033  letri  11034  ltadd2i  11036  mul02lem2  11082  addid1  11085  addcani  11098  addcan2i  11099  mul12i  11100  mul32i  11101  add12i  11127  add32i  11128  subaddi  11238  subadd2i  11239  subsub23i  11241  addsubassi  11242  addsubi  11243  subcani  11244  subcan2i  11245  pnncani  11246  subdii  11354  subdiri  11355  ltadd1i  11459  leadd1i  11460  leadd2i  11461  ltsubaddi  11462  lesubaddi  11463  ltsubadd2i  11464  lesubadd2i  11465  ltaddsubi  11466  mulcani  11544  div23i  11663  div11i  11664  1mhlfehlf  12122  halfpm6th  12124  3halfnz  12329  addex  12657  mulex  12658  unirnioo  13110  ioorebas  13112  xnn0xrge0  13167  fldiv4lem1div2  13485  uzenom  13612  nnenom  13628  seqexw  13665  m1expcl2  13732  i4  13849  expnass  13852  faclbnd4lem1  13935  bcn1  13955  hashfxnn0  13979  ccat2s1p1  14264  ccat2s1p2  14265  cats1fvn  14499  cats1fv  14500  cats1cat  14502  cats2cat  14503  wrdlen3s3  14590  abs3difi  15049  0.999...  15521  bpoly3  15696  ef01bndlem  15821  cos1bnd  15824  cos2bnd  15825  sin4lt0  15832  rpnnen2lem3  15853  rpnnen2lem11  15861  rpnnen  15864  rexpen  15865  aleph1irr  15883  3dvdsdec  15969  3dvds2dec  15970  divalglem2  16032  ndvdsi  16049  flodddiv4  16050  gcdaddmlem  16159  bezout  16179  3lcm2e6woprm  16248  6lcm4e12  16249  lcmf0  16267  lcmf2a3a4e12  16280  dec2dvds  16692  modxai  16697  modsubi  16701  gcdi  16702  numexp2x  16708  2exp5  16715  2exp11  16719  0symgefmndeq  18916  pmtrprfval  19010  m1expaddsub  19021  0frgp  19300  staffval  20022  cnfldcj  20517  cnfldds  20520  cnfldfun  20522  xrsadd  20527  xrsmul  20528  xrsds  20553  cnmgpid  20572  nn0srg  20580  rge0srg  20581  zring0  20592  cnmsgnsubg  20694  psgninv  20699  re0g  20729  ocvfval  20783  frlmbas  20872  mdetrlin  21659  mdetunilem9  21677  leordtval2  22271  iscnp2  22298  utop3cls  23311  nmfval  23650  nmoffn  23781  nmofval  23784  icccld  23836  addcnlem  23933  iimulcn  24007  icopnfhmeo  24012  iccpnfcnv  24013  iccpnfhmeo  24014  xrhmeo  24015  xrhmph  24016  oprpiece1res1  24020  oprpiece1res2  24021  ishtpy  24041  pcoass  24093  cnstrcvs  24210  cncvs  24214  recvs  24215  qcvs  24216  zclmncvs  24217  tcphex  24286  cnfldcusp  24426  resscdrg  24427  reust  24450  recusp  24451  vitalilem4  24680  vitalilem5  24681  mbfdm  24695  dveflem  25048  dvlipcn  25063  c1lip2  25067  dgrid  25330  iaa  25390  abelthlem3  25497  abelthlem5  25499  abelth  25505  efcn  25507  sinhalfpilem  25525  sincosq1lem  25559  sincosq4sgn  25563  tangtx  25567  sincos4thpi  25575  sincos6thpi  25577  pigt3  25579  pige3ALT  25581  cos0pilt1  25593  relogcn  25698  dvlog2lem  25712  dvlog2  25713  logtayl  25720  logtayl2  25722  cxpsqrtlem  25762  cxpsqrt  25763  2irrexpq  25790  cxpcn2  25804  cxpcn3  25806  logblog  25847  2logb9irr  25850  2logb3irr  25852  2logb9irrALT  25853  sqrt2cxp2logb9e3  25854  2irrexpqALT  25855  ang180lem1  25864  ang180lem2  25865  1cubrlem  25896  mcubic  25902  quart1lem  25910  quart1  25911  reasinsin  25951  atancj  25965  efiatan  25967  atantan  25978  atanbndlem  25980  atan1  25983  atancn  25991  atantayl2  25993  log2cnv  25999  log2tlbnd  26000  log2ublem1  26001  log2ublem2  26002  log2ub  26004  efrlim  26024  scvxcvx  26040  1sgm2ppw  26253  ppiub  26257  bclbnd  26333  bposlem8  26344  lgsdir2lem1  26378  lgsdir2lem5  26382  lgseisenlem1  26428  lgseisenlem2  26429  lgsquadlem1  26433  chebbnd1  26525  dchrvmasumlem2  26551  istrkg3ld  26726  trgcgrg  26780  ax5seglem7  27206  axlowdimlem6  27218  axlowdimlem8  27220  axlowdimlem11  27223  elntg2  27256  cusgrsizeindb1  27720  vtxdginducedm1  27813  0grrusgr  27849  erclwwlktr  28287  erclwwlkntr  28336  wlk2v2e  28422  upgr3v3e3cycl  28445  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  konigsberglem5  28521  ex-fl  28712  ex-mod  28714  ex-hash  28718  ex-lcm  28723  0vfval  28869  smcnlem  28960  lnocoi  29020  nmlno0lem  29056  nmblolbii  29062  blocnilem  29067  blocni  29068  cncph  29082  isph  29085  ip0i  29088  ip1ilem  29089  ip2i  29091  ipdirilem  29092  ipasslem7  29099  ipasslem8  29100  ipasslem9  29101  ipasslem10  29102  ipasslem11  29103  ip2dii  29107  pythi  29113  siilem1  29114  siilem2  29115  siii  29116  hvmulassi  29309  hvmulcomi  29310  hvdistr1i  29314  hvsubdistr1i  29315  hvassi  29316  hvadd32i  29317  hvsubassi  29318  hvsub32i  29319  normlem0  29372  normlem8  29380  normlem9  29381  bcseqi  29383  polid2i  29420  hhph  29441  hlim0  29498  shscli  29580  shlessi  29640  shlej1i  29641  omlsilem  29665  shlubi  29678  h1de2i  29816  pjadjii  29937  pjaddii  29938  pjmulii  29940  pjdifnormii  29946  pjcji  29947  hoaddsubassi  30083  eigrei  30097  eigposi  30099  eigorthi  30100  adj0  30257  lnopeq0lem1  30268  lnopunilem1  30273  lnophmlem2  30280  nmcexi  30289  nmcopexi  30290  lnfn0i  30305  nmcfnexi  30314  mdexchi  30598  xppreima2  30889  dp2clq  31057  dp2lt  31061  dp2ltc  31063  dpexpp1  31084  dpmul  31089  dpmul4  31090  elxrge02  31108  xrge0adddir  31203  psgnid  31266  cnmsgn0g  31315  altgnsg  31318  xrnarchi  31340  xrge0slmod  31450  znfermltl  31464  ccfldextdgrr  31644  raddcn  31781  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhmeo  31788  xrge0iifhom  31789  xrge0iifmhm  31791  xrge0mulc1cn  31793  lmlimxrge0  31800  pnfneige0  31803  lmxrge0  31804  zringnm  31810  rezh  31821  qqh0  31834  qqh1  31835  qqhucn  31842  esumpinfval  31941  hashf2  31952  esumcvg  31954  br2base  32136  sxbrsigalem3  32139  dya2iocbrsiga  32142  dya2icobrsiga  32143  sxbrsigalem1  32152  sxbrsigalem2  32153  sxbrsigalem4  32154  sxbrsigalem5  32155  sxbrsiga  32157  ballotlem2  32355  ballotlem4  32365  ballotlemi1  32369  ballotth  32404  sgnclre  32406  signstf  32445  itgexpif  32486  chtvalz  32509  hgt750lemd  32528  hgt750lem  32531  tgoldbachgnn  32539  lfuhgr2  32980  subfacp1lem1  33041  subfacp1lem6  33047  kur14lem6  33073  cvmliftlem4  33150  satf0suc  33238  problem4  33526  quad3  33528  logi  33606  iexpire  33607  fununiq  33649  on2recsfn  33753  norecfn  34030  norec2fn  34040  fvtransport  34261  bj-minftyccb  35323  taupilem2  35420  iccioo01  35425  1oequni2o  35466  finxp1o  35490  finxpreclem4  35492  cos2h  35695  tan2h  35696  poimirlem9  35713  poimirlem27  35731  poimirlem28  35732  ismblfin  35745  mbfposadd  35751  ftc1anclem5  35781  asindmre  35787  dvasin  35788  dvacos  35789  rrnval  35912  el3v  36298  dihjatcclem4  39362  lcmineqlem12  39976  sn-00idlem2  40303  sn-00id  40305  remul02  40309  rei4  40326  sn-0lt1  40353  rabren3dioph  40553  jm2.27dlem2  40748  rmydioph  40752  rmxdioph  40754  expdiophlem2  40760  expdioph  40761  arearect  40962  areaquad  40963  corclrcl  41204  iunrelexpuztr  41216  corcltrcl  41236  dffrege76  41436  k0004val0  41653  lhe4.4ex1a  41836  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  ax6e2ndeqALT  42440  sineq0ALT  42446  pnfel0pnf  42956  lptioo2cn  43076  limsup10ex  43204  liminf10ex  43205  icccncfext  43318  itgsin0pilem1  43381  itgsbtaddcnst  43413  stoweidlem13  43444  wallispilem2  43497  wallispilem4  43499  wallispi2lem1  43502  stirlinglem13  43517  dirkerper  43527  dirkertrigeqlem3  43531  dirkeritg  43533  dirkercncflem1  43534  dirkercncflem4  43537  fourierdlem42  43580  fourierdlem62  43599  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  sqwvfoura  43659  fourierswlem  43661  fouriersw  43662  smfmullem4  44215  fmtnoprmfac2lem1  44906  fmtno4prm  44915  3exp4mod41  44956  41prothprmlem2  44958  6gbe  45111  7gbow  45112  8gbe  45113  9gbo  45114  11gbo  45115  sbgoldbalt  45121  nnsum4primesevenALTV  45141  0nodd  45252  oddinmgm  45257  2zrng0  45384  zlmodzxz0  45580  zlmodzxzequa  45725  zlmodzxzequap  45728  zlmodzxzldeplem3  45731  nnlog2ge0lt1  45800  blen1  45818  blen2  45819  nnolog2flm1  45824  ackval42  45930  ehl2eudisval0  45959  line2ylem  45985  i0oii  46101  io1ii  46102  sepfsepc  46109