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  6534  feq12i  6663  ftp  7111  caovass  7569  caovdi  7588  ordom  7832  mptexw  7911  ofmres  7942  sbcoteq1a  8009  mpoexw  8036  xpord3lem  8105  omopthlem1  8600  omopthlem2  8601  omopthi  8602  on2recsfn  8608  xpcomen  9009  snnen2o  9161  unfilem3  9232  hartogs  9473  card2on  9483  unwf  9739  inlresf1  9844  inrresf1  9846  tskwe  9879  alephsmo  10031  dfac4  10051  dfac2a  10059  ackbij1lem13  10160  axdc2lem  10377  axcclem  10386  ondomon  10492  cfpwsdom  10513  pwfseqlem2  10588  pwfseqlem3  10589  1lt2pi  10834  addassi  11160  mulassi  11161  adddii  11162  adddiri  11163  lttri  11276  lelttri  11277  ltletri  11278  letri  11279  ltadd2i  11281  mul02lem2  11327  addrid  11330  addcani  11343  addcan2i  11344  mul12i  11345  mul32i  11346  add12i  11373  add32i  11374  subaddi  11485  subadd2i  11486  subsub23i  11488  addsubassi  11489  addsubi  11490  subcani  11491  subcan2i  11492  pnncani  11493  subdii  11603  subdiri  11604  ltadd1i  11708  leadd1i  11709  leadd2i  11710  ltsubaddi  11711  lesubaddi  11712  ltsubadd2i  11713  lesubadd2i  11714  ltaddsubi  11715  mulcani  11793  div23i  11916  div11i  11917  3halfnz  12589  mpoaddex  12923  addex  12924  mpomulex  12925  mulex  12926  unirnioo  13386  ioorebas  13388  xnn0xrge0  13443  fldiv4lem1div2  13775  uzenom  13905  nnenom  13921  seqexw  13958  m1expcl2  14026  i4  14145  expnass  14149  faclbnd4lem1  14234  bcn1  14254  hashfxnn0  14278  ccat2s1p1  14570  ccat2s1p2  14571  cats1fvn  14800  cats1fv  14801  cats1cat  14803  cats2cat  14804  wrdlen3s3  14891  abs3difi  15352  0.999...  15823  bpoly3  16000  ef01bndlem  16128  cos1bnd  16131  cos2bnd  16132  sin4lt0  16139  rpnnen2lem3  16160  rpnnen2lem11  16168  rpnnen  16171  rexpen  16172  aleph1irr  16190  3dvdsdec  16278  3dvds2dec  16279  divalglem2  16341  ndvdsi  16358  flodddiv4  16361  gcdaddmlem  16470  bezout  16489  3lcm2e6woprm  16561  6lcm4e12  16562  lcmf0  16580  lcmf2a3a4e12  16593  dec2dvds  17010  modxai  17015  modsubi  17019  gcdi  17020  numexp2x  17025  2exp5  17032  2exp11  17036  0symgefmndeq  19308  pmtrprfval  19401  m1expaddsub  19412  0frgp  19693  staffval  20761  cnfldcj  21305  cnfldds  21308  cnfldfunALT  21311  cnfldcjOLD  21318  cnflddsOLD  21321  cnfldfunALTOLD  21324  xrsadd  21327  xrsmul  21328  xrsds  21351  cnmgpid  21371  nn0srg  21379  rge0srg  21380  zring0  21400  pzriprnglem13  21435  pzriprng1ALT  21438  fermltlchr  21471  cnmsgnsubg  21519  psgninv  21524  re0g  21554  ocvfval  21608  frlmbas  21697  mdetrlin  22522  mdetunilem9  22540  leordtval2  23132  iscnp2  23159  utop3cls  24172  nmfval  24509  nmoffn  24632  nmofval  24635  icccld  24687  addcnlem  24786  iimulcn  24867  iimulcnOLD  24868  icopnfhmeo  24874  iccpnfcnv  24875  iccpnfhmeo  24876  xrhmeo  24877  xrhmph  24878  oprpiece1res1  24882  oprpiece1res2  24883  ishtpy  24904  pcoass  24957  cnstrcvs  25074  cncvs  25078  recvs  25079  qcvs  25080  zclmncvs  25081  tcphex  25150  cnfldcusp  25290  resscdrg  25291  reust  25314  recusp  25315  vitalilem4  25545  vitalilem5  25546  mbfdm  25560  dveflem  25916  dvlipcn  25932  c1lip2  25936  dgrid  26203  iaa  26266  abelthlem3  26376  abelthlem5  26378  abelth  26384  efcn  26386  sinhalfpilem  26405  sincosq1lem  26439  sincosq4sgn  26443  tangtx  26447  sincos4thpi  26455  sincos6thpi  26458  pigt3  26460  pige3ALT  26462  cos0pilt1  26474  logi  26529  relogcn  26580  dvlog2lem  26594  dvlog2  26595  logtayl  26602  logtayl2  26604  cxpsqrtlem  26644  cxpsqrt  26645  2irrexpq  26673  cxpcn2  26689  cxpcn3  26691  logblog  26735  2logb9irr  26738  2logb3irr  26740  2logb9irrALT  26741  sqrt2cxp2logb9e3  26742  2irrexpqALT  26743  ang180lem1  26752  ang180lem2  26753  1cubrlem  26784  mcubic  26790  quart1lem  26798  quart1  26799  reasinsin  26839  atancj  26853  efiatan  26855  atantan  26866  atanbndlem  26868  atan1  26871  atancn  26879  atantayl2  26881  log2cnv  26887  log2tlbnd  26888  log2ublem1  26889  log2ublem2  26890  log2ub  26892  efrlim  26912  efrlimOLD  26913  scvxcvx  26929  1sgm2ppw  27144  ppiub  27148  bclbnd  27224  bposlem8  27235  lgsdir2lem1  27269  lgsdir2lem5  27273  lgseisenlem1  27319  lgseisenlem2  27320  lgsquadlem1  27324  chebbnd1  27416  dchrvmasumlem2  27442  norecfn  27893  norec2fn  27903  addsproplem2  27917  addsproplem6  27921  addsbdaylem  27963  negs1s  27973  negsproplem2  27975  mulsproplem2  28060  mulsproplem3  28061  mulsproplem5  28063  mulsproplem6  28064  mulsproplem7  28065  mulsproplem8  28066  mulsproplem13  28071  mulsproplem14  28072  0zs  28316  zseo  28349  twocut  28350  istrkg3ld  28441  trgcgrg  28495  ax5seglem7  28915  axlowdimlem6  28927  axlowdimlem8  28929  axlowdimlem11  28932  elntg2  28965  cusgrsizeindb1  29431  vtxdginducedm1  29524  0grrusgr  29560  erclwwlktr  30001  erclwwlkntr  30050  wlk2v2e  30136  upgr3v3e3cycl  30159  konigsberglem1  30231  konigsberglem2  30232  konigsberglem3  30233  konigsberglem5  30235  ex-fl  30426  ex-mod  30428  ex-hash  30432  ex-lcm  30437  0vfval  30585  smcnlem  30676  lnocoi  30736  nmlno0lem  30772  nmblolbii  30778  blocnilem  30783  blocni  30784  cncph  30798  isph  30801  ip0i  30804  ip1ilem  30805  ip2i  30807  ipdirilem  30808  ipasslem7  30815  ipasslem8  30816  ipasslem9  30817  ipasslem10  30818  ipasslem11  30819  ip2dii  30823  pythi  30829  siilem1  30830  siilem2  30831  siii  30832  hvmulassi  31025  hvmulcomi  31026  hvdistr1i  31030  hvsubdistr1i  31031  hvassi  31032  hvadd32i  31033  hvsubassi  31034  hvsub32i  31035  normlem0  31088  normlem8  31096  normlem9  31097  bcseqi  31099  polid2i  31136  hhph  31157  hlim0  31214  shscli  31296  shlessi  31356  shlej1i  31357  omlsilem  31381  shlubi  31394  h1de2i  31532  pjadjii  31653  pjaddii  31654  pjmulii  31656  pjdifnormii  31662  pjcji  31663  hoaddsubassi  31799  eigrei  31813  eigposi  31815  eigorthi  31816  adj0  31973  lnopeq0lem1  31984  lnopunilem1  31989  lnophmlem2  31996  nmcexi  32005  nmcopexi  32006  lnfn0i  32021  nmcfnexi  32030  mdexchi  32314  xppreima2  32625  sgnclre  32807  dp2clq  32851  dp2lt  32855  dp2ltc  32857  dpexpp1  32878  dpmul  32883  dpmul4  32884  elxrge02  32902  xrge0adddir  33002  psgnid  33069  cnmsgn0g  33118  altgnsg  33121  xrnarchi  33153  xrge0slmod  33312  znfermltl  33330  ccfldextdgrr  33660  cos9thpiminplylem4  33768  cos9thpiminplylem5  33769  raddcn  33912  xrge0iifcnv  33916  xrge0iifiso  33918  xrge0iifhmeo  33919  xrge0iifhom  33920  xrge0iifmhm  33922  xrge0mulc1cn  33924  lmlimxrge0  33931  pnfneige0  33934  lmxrge0  33935  zringnm  33941  rezh  33952  qqh0  33967  qqh1  33968  qqhucn  33975  esumpinfval  34056  hashf2  34067  esumcvg  34069  br2base  34253  sxbrsigalem3  34256  dya2iocbrsiga  34259  dya2icobrsiga  34260  sxbrsigalem1  34269  sxbrsigalem2  34270  sxbrsigalem4  34271  sxbrsigalem5  34272  sxbrsiga  34274  ballotlem2  34473  ballotlem4  34483  ballotlemi1  34487  ballotth  34522  signstf  34550  itgexpif  34590  chtvalz  34613  hgt750lemd  34632  hgt750lem  34635  tgoldbachgnn  34643  lfuhgr2  35099  subfacp1lem1  35159  subfacp1lem6  35165  kur14lem6  35191  cvmliftlem4  35268  satf0suc  35356  problem4  35648  quad3  35650  iexpire  35715  fununiq  35749  fvtransport  36013  bj-minftyccb  37206  taupilem2  37303  iccioo01  37308  1oequni2o  37349  finxp1o  37373  finxpreclem4  37375  cos2h  37598  tan2h  37599  poimirlem9  37616  poimirlem27  37634  poimirlem28  37635  ismblfin  37648  mbfposadd  37654  ftc1anclem5  37684  asindmre  37690  dvasin  37691  dvacos  37692  rrnval  37814  dihjatcclem4  41408  lcmineqlem12  42021  fisdomnn  42225  subex  42228  absex  42229  cjex  42230  cxpi11d  42324  redvmptabs  42341  readvrec  42343  sn-00idlem2  42380  sn-00id  42382  remul02  42386  rabren3dioph  42796  jm2.27dlem2  42992  rmydioph  42996  rmxdioph  42998  expdiophlem2  43004  expdioph  43005  arearect  43197  areaquad  43198  2omomeqom  43285  omnord1ex  43286  corclrcl  43689  iunrelexpuztr  43701  corcltrcl  43721  dffrege76  43921  k0004val0  44136  lhe4.4ex1a  44311  binomcxplemdvbinom  44335  binomcxplemnotnn0  44338  ax6e2ndeqALT  44913  sineq0ALT  44919  nregmodelf1o  44998  pnfel0pnf  45519  lptioo2cn  45636  limsup10ex  45764  liminf10ex  45765  icccncfext  45878  itgsin0pilem1  45941  itgsbtaddcnst  45973  stoweidlem13  46004  wallispilem2  46057  wallispilem4  46059  wallispi2lem1  46062  stirlinglem13  46077  dirkerper  46087  dirkertrigeqlem3  46091  dirkeritg  46093  dirkercncflem1  46094  dirkercncflem4  46097  fourierdlem42  46140  fourierdlem62  46159  fourierdlem102  46199  fourierdlem103  46200  fourierdlem104  46201  fourierdlem114  46211  sqwvfoura  46219  fourierswlem  46221  fouriersw  46222  smfmullem4  46785  ceil5half3  47334  8mod5e3  47354  fmtnoprmfac2lem1  47560  fmtno4prm  47569  3exp4mod41  47610  41prothprmlem2  47612  6gbe  47765  7gbow  47766  8gbe  47767  9gbo  47768  11gbo  47769  sbgoldbalt  47775  nnsum4primesevenALTV  47795  usgrexmpl2nb0  48015  usgrexmpl2nb3  48018  gpg3nbgrvtx0  48060  gpg3nbgrvtx0ALT  48061  gpg3nbgrvtx1  48062  gpg5grlic  48077  0nodd  48151  oddinmgm  48156  2zrng0  48225  zlmodzxz0  48337  zlmodzxzequa  48478  zlmodzxzequap  48481  zlmodzxzldeplem3  48484  nnlog2ge0lt1  48548  blen1  48566  blen2  48567  nnolog2flm1  48572  ackval42  48678  ehl2eudisval0  48707  line2ylem  48733  i0oii  48901  io1ii  48902  sepfsepc  48909  rescofuf  49075  setc1ohomfval  49475  setc1ocofval  49476