Theorem mp3an 1440

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

Syntax hints:   → wi 4   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  raltp  4516  rextp  4517  opthhausdorff  5264  funopg  6224  feq12i  6339  ftp  6744  caovass  7166  caovdi  7185  ordom  7407  mptexw  7468  ofmres  7499  mpoexw  7586  omopthlem1  8084  omopthlem2  8085  omopthi  8086  xpcomen  8406  unfilem3  8581  hartogs  8805  card2on  8815  unwf  9035  inlresf1  9140  inrresf1  9142  tskwe  9175  alephsmo  9324  dfac4  9344  dfac2a  9351  ackbij1lem13  9454  axdc2lem  9670  axcclem  9679  ondomon  9785  cfpwsdom  9806  pwfseqlem2  9881  pwfseqlem3  9882  1lt2pi  10127  addassi  10452  mulassi  10453  adddii  10454  adddiri  10455  lttri  10568  lelttri  10569  ltletri  10570  letri  10571  ltadd2i  10573  mul02lem2  10619  addid1  10622  addcani  10635  addcan2i  10636  mul12i  10637  mul32i  10638  add12i  10664  add32i  10665  subaddi  10776  subadd2i  10777  subsub23i  10779  addsubassi  10780  addsubi  10781  subcani  10782  subcan2i  10783  pnncani  10784  subdii  10892  subdiri  10893  ltadd1i  10997  leadd1i  10998  leadd2i  10999  ltsubaddi  11000  lesubaddi  11001  ltsubadd2i  11002  lesubadd2i  11003  ltaddsubi  11004  mulcani  11082  div23i  11201  div11i  11202  1mhlfehlf  11669  halfpm6th  11671  3halfnz  11877  addex  12205  mulex  12206  unirnioo  12656  ioorebas  12658  xnn0xrge0  12710  fldiv4lem1div2  13025  uzenom  13150  nnenom  13166  seqexw  13203  m1expcl2  13269  i4  13385  expnass  13388  faclbnd4lem1  13471  bcn1  13491  hashfxnn0  13515  cats1fvn  14085  cats1fv  14086  cats1cat  14088  cats2cat  14089  wrdlen3s3  14176  abs3difi  14633  0.999...  15100  bpoly3  15275  ef01bndlem  15400  cos1bnd  15403  cos2bnd  15404  sin4lt0  15411  rpnnen2lem3  15432  rpnnen2lem11  15440  rpnnen  15443  rexpen  15444  aleph1irr  15462  3dvdsdec  15544  3dvds2dec  15545  divalglem2  15609  ndvdsi  15626  flodddiv4  15627  gcdaddmlem  15735  bezout  15750  3lcm2e6woprm  15818  6lcm4e12  15819  lcmf0  15837  lcmf2a3a4e12  15850  dec2dvds  16258  modxai  16263  modsubi  16267  gcdi  16268  numexp2x  16274  prdsval  16587  prdsds  16596  plusffval  17718  pmtrprfval  18379  m1expaddsub  18391  0frgp  18668  staffval  19343  scaffval  19377  cnfldcj  20257  cnfldds  20260  cnfldfun  20262  xrsadd  20267  xrsmul  20268  xrsds  20293  cnmgpid  20312  nn0srg  20320  rge0srg  20321  zring0  20332  cnmsgnsubg  20426  psgninv  20431  re0g  20461  ipffval  20497  ocvfval  20515  frlmbas  20604  mdetrlin  20918  mdetunilem9  20936  leordtval2  21527  iscnp2  21554  utop3cls  22566  nmfval  22904  nmoffn  23026  nmofval  23029  icccld  23081  addcnlem  23178  iimulcn  23248  icopnfhmeo  23253  iccpnfcnv  23254  iccpnfhmeo  23255  xrhmeo  23256  xrhmph  23257  oprpiece1res1  23261  oprpiece1res2  23262  ishtpy  23282  pcoass  23334  cnstrcvs  23451  cncvs  23455  recvs  23456  qcvs  23457  zclmncvs  23458  tcphex  23526  cnfldcusp  23666  resscdrg  23667  reust  23690  recusp  23691  vitalilem4  23918  vitalilem5  23919  mbfdm  23933  dveflem  24282  dvlipcn  24297  c1lip2  24301  dgrid  24560  iaa  24620  abelthlem3  24727  abelthlem5  24729  abelth  24735  efcn  24737  sinhalfpilem  24755  sincosq1lem  24789  sincosq4sgn  24793  tangtx  24797  sincos4thpi  24805  sincos6thpi  24807  pigt3  24809  pige3ALT  24811  relogcn  24925  dvlog2lem  24939  dvlog2  24940  logtayl  24947  logtayl2  24949  cxpsqrtlem  24989  cxpsqrt  24990  2irrexpq  25017  cxpcn2  25031  cxpcn3  25033  logblog  25074  2logb9irr  25077  2logb3irr  25079  2logb9irrALT  25080  sqrt2cxp2logb9e3  25081  2irrexpqALT  25082  ang180lem1  25091  ang180lem2  25092  1cubrlem  25123  mcubic  25129  quart1lem  25137  quart1  25138  reasinsin  25178  atancj  25192  efiatan  25194  atantan  25205  atanbndlem  25207  atan1  25210  atancn  25218  atantayl2  25220  log2cnv  25227  log2tlbnd  25228  log2ublem1  25229  log2ublem2  25230  log2ub  25232  efrlim  25252  scvxcvx  25268  1sgm2ppw  25481  ppiub  25485  bclbnd  25561  bposlem8  25572  lgsdir2lem1  25606  lgsdir2lem5  25610  lgseisenlem1  25656  lgseisenlem2  25657  lgsquadlem1  25661  chebbnd1  25753  dchrvmasumlem2  25779  istrkg3ld  25952  trgcgrg  26006  ax5seglem7  26427  axlowdimlem6  26439  axlowdimlem8  26441  axlowdimlem11  26444  elntg2  26477  cusgrsizeindb1  26938  vtxdginducedm1  27031  0grrusgr  27067  erclwwlktr  27540  erclwwlkntr  27598  wlk2v2e  27689  upgr3v3e3cycl  27712  konigsberglem1  27787  konigsberglem2  27788  konigsberglem3  27789  konigsberglem5  27791  ex-fl  28007  ex-mod  28009  ex-hash  28013  ex-lcm  28018  0vfval  28163  smcnlem  28254  lnocoi  28314  nmlno0lem  28350  nmblolbii  28356  blocnilem  28361  blocni  28362  cncph  28376  isph  28379  ip0i  28382  ip1ilem  28383  ip2i  28385  ipdirilem  28386  ipasslem7  28393  ipasslem8  28394  ipasslem9  28395  ipasslem10  28396  ipasslem11  28397  ip2dii  28401  pythi  28407  siilem1  28408  siilem2  28409  siii  28410  hvmulassi  28605  hvmulcomi  28606  hvdistr1i  28610  hvsubdistr1i  28611  hvassi  28612  hvadd32i  28613  hvsubassi  28614  hvsub32i  28615  normlem0  28668  normlem8  28676  normlem9  28677  bcseqi  28679  polid2i  28716  hhph  28737  hlim0  28794  shscli  28878  shlessi  28938  shlej1i  28939  omlsilem  28963  shlubi  28976  h1de2i  29114  pjadjii  29235  pjaddii  29236  pjmulii  29238  pjdifnormii  29244  pjcji  29245  hoaddsubassi  29381  eigrei  29395  eigposi  29397  eigorthi  29398  adj0  29555  lnopeq0lem1  29566  lnopunilem1  29571  lnophmlem2  29578  nmcexi  29587  nmcopexi  29588  lnfn0i  29603  nmcfnexi  29612  mdexchi  29896  xppreima2  30160  dp2clq  30306  dp2lt  30310  dp2ltc  30312  dpexpp1  30333  dpmul  30338  dpmul4  30339  elxrge02  30357  xrge0adddir  30411  psgnid  30461  altgnsg  30465  xrnarchi  30479  xrge0slmod  30596  ccfldextdgrr  30686  raddcn  30816  xrge0iifcnv  30820  xrge0iifiso  30822  xrge0iifhmeo  30823  xrge0iifhom  30824  xrge0iifmhm  30826  xrge0mulc1cn  30828  lmlimxrge0  30835  pnfneige0  30838  lmxrge0  30839  zringnm  30845  rezh  30856  qqh0  30869  qqh1  30870  qqhucn  30877  esumpinfval  30976  hashf2  30987  esumcvg  30989  br2base  31172  sxbrsigalem3  31175  dya2iocbrsiga  31178  dya2icobrsiga  31179  sxbrsigalem1  31188  sxbrsigalem2  31189  sxbrsigalem4  31190  sxbrsigalem5  31191  sxbrsiga  31193  ballotlem2  31392  ballotlem4  31402  ballotlemi1  31406  ballotth  31441  sgnclre  31443  signstf  31482  itgexpif  31525  chtvalz  31548  hgt750lemd  31567  hgt750lem  31570  tgoldbachgnn  31578  subfacp1lem1  32011  subfacp1lem6  32017  kur14lem6  32043  cvmliftlem4  32120  satf0suc  32186  problem4  32431  quad3  32433  logi  32486  iexpire  32487  fununiq  32532  fvtransport  33014  bj-minftyccb  33976  taupilem2  34045  1oequni2o  34091  finxp1o  34114  finxpreclem4  34116  cos2h  34324  tan2h  34325  poimirlem9  34342  poimirlem27  34360  poimirlem28  34361  ismblfin  34374  mbfposadd  34380  ftc1anclem5  34412  asindmre  34418  dvasin  34419  dvacos  34420  rrnval  34547  el3v  34935  dihjatcclem4  38002  rabren3dioph  38808  jm2.27dlem2  39003  rmydioph  39007  rmxdioph  39009  expdiophlem2  39015  expdioph  39016  arearect  39218  areaquad  39219  corclrcl  39415  iunrelexpuztr  39427  corcltrcl  39447  dffrege76  39648  k0004val0  39867  lhe4.4ex1a  40077  binomcxplemdvbinom  40101  binomcxplemnotnn0  40104  ax6e2ndeqALT  40684  sineq0ALT  40690  pnfel0pnf  41236  lptioo2cn  41358  limsup10ex  41486  liminf10ex  41487  icccncfext  41601  itgsin0pilem1  41666  itgsbtaddcnst  41698  stoweidlem13  41730  wallispilem2  41783  wallispilem4  41785  wallispi2lem1  41788  stirlinglem13  41803  dirkerper  41813  dirkertrigeqlem3  41817  dirkeritg  41819  dirkercncflem1  41820  dirkercncflem4  41823  fourierdlem42  41866  fourierdlem62  41885  fourierdlem102  41925  fourierdlem103  41926  fourierdlem104  41927  fourierdlem114  41937  sqwvfoura  41945  fourierswlem  41947  fouriersw  41948  smfmullem4  42501  fmtnoprmfac2lem1  43097  fmtno4prm  43106  2exp5  43124  2exp11  43134  3exp4mod41  43150  41prothprmlem2  43152  6gbe  43305  7gbow  43306  8gbe  43307  9gbo  43308  11gbo  43309  sbgoldbalt  43315  nnsum4primesevenALTV  43335  0nodd  43446  oddinmgm  43451  2zrng0  43574  zlmodzxz0  43769  zlmodzxzequa  43919  zlmodzxzequap  43922  zlmodzxzldeplem3  43925  nnlog2ge0lt1  43995  blen1  44013  blen2  44014  nnolog2flm1  44019  ehl2eudisval0  44081  line2ylem  44107