Theorem mp3an 1463

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

Syntax hints:   → wi 4   ∧ w3a 1086

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

This theorem is referenced by:  el3v  3452  raltp  4665  rextp  4666  opthhausdorff  5472  funopg  6535  feq12i  6664  ftp  7112  caovass  7570  caovdi  7589  ordom  7833  mptexw  7912  ofmres  7943  sbcoteq1a  8010  mpoexw  8037  xpord3lem  8106  omopthlem1  8601  omopthlem2  8602  omopthi  8603  on2recsfn  8609  xpcomen  9010  snnen2o  9162  unfilem3  9233  hartogs  9474  card2on  9484  unwf  9742  inlresf1  9847  inrresf1  9849  tskwe  9882  alephsmo  10034  dfac4  10054  dfac2a  10062  ackbij1lem13  10163  axdc2lem  10380  axcclem  10389  ondomon  10495  cfpwsdom  10516  pwfseqlem2  10591  pwfseqlem3  10592  1lt2pi  10837  addassi  11163  mulassi  11164  adddii  11165  adddiri  11166  lttri  11279  lelttri  11280  ltletri  11281  letri  11282  ltadd2i  11284  mul02lem2  11330  addrid  11333  addcani  11346  addcan2i  11347  mul12i  11348  mul32i  11349  add12i  11376  add32i  11377  subaddi  11488  subadd2i  11489  subsub23i  11491  addsubassi  11492  addsubi  11493  subcani  11494  subcan2i  11495  pnncani  11496  subdii  11606  subdiri  11607  ltadd1i  11711  leadd1i  11712  leadd2i  11713  ltsubaddi  11714  lesubaddi  11715  ltsubadd2i  11716  lesubadd2i  11717  ltaddsubi  11718  mulcani  11796  div23i  11919  div11i  11920  3halfnz  12592  mpoaddex  12926  addex  12927  mpomulex  12928  mulex  12929  unirnioo  13389  ioorebas  13391  xnn0xrge0  13446  fldiv4lem1div2  13778  uzenom  13908  nnenom  13924  seqexw  13961  m1expcl2  14029  i4  14148  expnass  14152  faclbnd4lem1  14237  bcn1  14257  hashfxnn0  14281  ccat2s1p1  14573  ccat2s1p2  14574  cats1fvn  14802  cats1fv  14803  cats1cat  14805  cats2cat  14806  wrdlen3s3  14893  abs3difi  15354  0.999...  15825  bpoly3  16002  ef01bndlem  16130  cos1bnd  16133  cos2bnd  16134  sin4lt0  16141  rpnnen2lem3  16162  rpnnen2lem11  16170  rpnnen  16173  rexpen  16174  aleph1irr  16192  3dvdsdec  16280  3dvds2dec  16281  divalglem2  16343  ndvdsi  16360  flodddiv4  16363  gcdaddmlem  16472  bezout  16491  3lcm2e6woprm  16563  6lcm4e12  16564  lcmf0  16582  lcmf2a3a4e12  16595  dec2dvds  17012  modxai  17017  modsubi  17021  gcdi  17022  numexp2x  17027  2exp5  17034  2exp11  17038  0symgefmndeq  19310  pmtrprfval  19403  m1expaddsub  19414  0frgp  19695  staffval  20763  cnfldcj  21307  cnfldds  21310  cnfldfunALT  21313  cnfldcjOLD  21320  cnflddsOLD  21323  cnfldfunALTOLD  21326  xrsadd  21329  xrsmul  21330  xrsds  21353  cnmgpid  21373  nn0srg  21381  rge0srg  21382  zring0  21402  pzriprnglem13  21437  pzriprng1ALT  21440  fermltlchr  21473  cnmsgnsubg  21521  psgninv  21526  re0g  21556  ocvfval  21610  frlmbas  21699  mdetrlin  22524  mdetunilem9  22542  leordtval2  23134  iscnp2  23161  utop3cls  24174  nmfval  24511  nmoffn  24634  nmofval  24637  icccld  24689  addcnlem  24788  iimulcn  24869  iimulcnOLD  24870  icopnfhmeo  24876  iccpnfcnv  24877  iccpnfhmeo  24878  xrhmeo  24879  xrhmph  24880  oprpiece1res1  24884  oprpiece1res2  24885  ishtpy  24906  pcoass  24959  cnstrcvs  25076  cncvs  25080  recvs  25081  qcvs  25082  zclmncvs  25083  tcphex  25152  cnfldcusp  25292  resscdrg  25293  reust  25316  recusp  25317  vitalilem4  25547  vitalilem5  25548  mbfdm  25562  dveflem  25918  dvlipcn  25934  c1lip2  25938  dgrid  26205  iaa  26268  abelthlem3  26378  abelthlem5  26380  abelth  26386  efcn  26388  sinhalfpilem  26407  sincosq1lem  26441  sincosq4sgn  26445  tangtx  26449  sincos4thpi  26457  sincos6thpi  26460  pigt3  26462  pige3ALT  26464  cos0pilt1  26476  logi  26531  relogcn  26582  dvlog2lem  26596  dvlog2  26597  logtayl  26604  logtayl2  26606  cxpsqrtlem  26646  cxpsqrt  26647  2irrexpq  26675  cxpcn2  26691  cxpcn3  26693  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  27895  norec2fn  27905  addsproplem2  27919  addsproplem6  27923  addsbdaylem  27965  negs1s  27975  negsproplem2  27977  mulsproplem2  28062  mulsproplem3  28063  mulsproplem5  28065  mulsproplem6  28066  mulsproplem7  28067  mulsproplem8  28068  mulsproplem13  28073  mulsproplem14  28074  0zs  28318  zseo  28351  twocut  28352  istrkg3ld  28443  trgcgrg  28497  ax5seglem7  28917  axlowdimlem6  28929  axlowdimlem8  28931  axlowdimlem11  28934  elntg2  28967  cusgrsizeindb1  29433  vtxdginducedm1  29526  0grrusgr  29562  erclwwlktr  30003  erclwwlkntr  30052  wlk2v2e  30138  upgr3v3e3cycl  30161  konigsberglem1  30233  konigsberglem2  30234  konigsberglem3  30235  konigsberglem5  30237  ex-fl  30428  ex-mod  30430  ex-hash  30434  ex-lcm  30439  0vfval  30587  smcnlem  30678  lnocoi  30738  nmlno0lem  30774  nmblolbii  30780  blocnilem  30785  blocni  30786  cncph  30800  isph  30803  ip0i  30806  ip1ilem  30807  ip2i  30809  ipdirilem  30810  ipasslem7  30817  ipasslem8  30818  ipasslem9  30819  ipasslem10  30820  ipasslem11  30821  ip2dii  30825  pythi  30831  siilem1  30832  siilem2  30833  siii  30834  hvmulassi  31027  hvmulcomi  31028  hvdistr1i  31032  hvsubdistr1i  31033  hvassi  31034  hvadd32i  31035  hvsubassi  31036  hvsub32i  31037  normlem0  31090  normlem8  31098  normlem9  31099  bcseqi  31101  polid2i  31138  hhph  31159  hlim0  31216  shscli  31298  shlessi  31358  shlej1i  31359  omlsilem  31383  shlubi  31396  h1de2i  31534  pjadjii  31655  pjaddii  31656  pjmulii  31658  pjdifnormii  31664  pjcji  31665  hoaddsubassi  31801  eigrei  31815  eigposi  31817  eigorthi  31818  adj0  31975  lnopeq0lem1  31986  lnopunilem1  31991  lnophmlem2  31998  nmcexi  32007  nmcopexi  32008  lnfn0i  32023  nmcfnexi  32032  mdexchi  32316  xppreima2  32627  sgnclre  32809  dp2clq  32853  dp2lt  32857  dp2ltc  32859  dpexpp1  32880  dpmul  32885  dpmul4  32886  elxrge02  32904  xrge0adddir  33004  psgnid  33071  cnmsgn0g  33120  altgnsg  33123  xrnarchi  33155  xrge0slmod  33314  znfermltl  33332  ccfldextdgrr  33662  cos9thpiminplylem4  33770  cos9thpiminplylem5  33771  raddcn  33914  xrge0iifcnv  33918  xrge0iifiso  33920  xrge0iifhmeo  33921  xrge0iifhom  33922  xrge0iifmhm  33924  xrge0mulc1cn  33926  lmlimxrge0  33933  pnfneige0  33936  lmxrge0  33937  zringnm  33943  rezh  33954  qqh0  33969  qqh1  33970  qqhucn  33977  esumpinfval  34058  hashf2  34069  esumcvg  34071  br2base  34255  sxbrsigalem3  34258  dya2iocbrsiga  34261  dya2icobrsiga  34262  sxbrsigalem1  34271  sxbrsigalem2  34272  sxbrsigalem4  34273  sxbrsigalem5  34274  sxbrsiga  34276  ballotlem2  34475  ballotlem4  34485  ballotlemi1  34489  ballotth  34524  signstf  34552  itgexpif  34592  chtvalz  34615  hgt750lemd  34634  hgt750lem  34637  tgoldbachgnn  34645  lfuhgr2  35101  subfacp1lem1  35161  subfacp1lem6  35167  kur14lem6  35193  cvmliftlem4  35270  satf0suc  35358  problem4  35650  quad3  35652  iexpire  35717  fununiq  35751  fvtransport  36015  bj-minftyccb  37208  taupilem2  37305  iccioo01  37310  1oequni2o  37351  finxp1o  37375  finxpreclem4  37377  cos2h  37600  tan2h  37601  poimirlem9  37618  poimirlem27  37636  poimirlem28  37637  ismblfin  37650  mbfposadd  37656  ftc1anclem5  37686  asindmre  37692  dvasin  37693  dvacos  37694  rrnval  37816  dihjatcclem4  41410  lcmineqlem12  42023  fisdomnn  42227  subex  42230  absex  42231  cjex  42232  cxpi11d  42326  redvmptabs  42343  readvrec  42345  sn-00idlem2  42382  sn-00id  42384  remul02  42388  rabren3dioph  42798  jm2.27dlem2  42994  rmydioph  42998  rmxdioph  43000  expdiophlem2  43006  expdioph  43007  arearect  43199  areaquad  43200  2omomeqom  43287  omnord1ex  43288  corclrcl  43691  iunrelexpuztr  43703  corcltrcl  43723  dffrege76  43923  k0004val0  44138  lhe4.4ex1a  44313  binomcxplemdvbinom  44337  binomcxplemnotnn0  44340  ax6e2ndeqALT  44915  sineq0ALT  44921  nregmodelf1o  45000  pnfel0pnf  45521  lptioo2cn  45638  limsup10ex  45766  liminf10ex  45767  icccncfext  45880  itgsin0pilem1  45943  itgsbtaddcnst  45975  stoweidlem13  46006  wallispilem2  46059  wallispilem4  46061  wallispi2lem1  46064  stirlinglem13  46079  dirkerper  46089  dirkertrigeqlem3  46093  dirkeritg  46095  dirkercncflem1  46096  dirkercncflem4  46099  fourierdlem42  46142  fourierdlem62  46161  fourierdlem102  46201  fourierdlem103  46202  fourierdlem104  46203  fourierdlem114  46213  sqwvfoura  46221  fourierswlem  46223  fouriersw  46224  smfmullem4  46787  ceil5half3  47336  8mod5e3  47356  fmtnoprmfac2lem1  47562  fmtno4prm  47571  3exp4mod41  47612  41prothprmlem2  47614  6gbe  47767  7gbow  47768  8gbe  47769  9gbo  47770  11gbo  47771  sbgoldbalt  47777  nnsum4primesevenALTV  47797  usgrexmpl2nb0  48017  usgrexmpl2nb3  48020  gpg3nbgrvtx0  48062  gpg3nbgrvtx0ALT  48063  gpg3nbgrvtx1  48064  gpg5grlic  48079  0nodd  48153  oddinmgm  48158  2zrng0  48227  zlmodzxz0  48339  zlmodzxzequa  48480  zlmodzxzequap  48483  zlmodzxzldeplem3  48486  nnlog2ge0lt1  48550  blen1  48568  blen2  48569  nnolog2flm1  48574  ackval42  48680  ehl2eudisval0  48709  line2ylem  48735  i0oii  48903  io1ii  48904  sepfsepc  48911  rescofuf  49077  setc1ohomfval  49477  setc1ocofval  49478