MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.2i Structured version   Visualization version   GIF version

Theorem pm3.2i 471
Description: Infer conjunction of premises. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
pm3.2i.1 𝜑
pm3.2i.2 𝜓
Assertion
Ref Expression
pm3.2i (𝜑𝜓)

Proof of Theorem pm3.2i
StepHypRef Expression
1 pm3.2i.1 . 2 𝜑
2 pm3.2i.2 . 2 𝜓
3 pm3.2 463 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
41, 2, 3mp2 9 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wa 384
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 197  df-an 386
This theorem is referenced by:  pm4.87  607  dfbi  660  mp4an  708  3pm3.2i  1237  unssi  3772  ssini  3820  bm1.3ii  4754  epelg  4996  elvv  5148  relopabi  5215  funpr  5912  funcnvpr  5918  mpt2v  6715  caovcom  6796  snnex  6930  pwnex  6932  1st2val  7154  2nd2val  7155  elxp7  7161  mptmpt2opabbrd  7208  wfrlem13  7387  wfr3  7395  tfr1a  7450  oeoa  7637  oeoe  7639  erov  7804  endisj  8007  phplem2  8100  snopfsupp  8258  r1funlim  8589  dfac2  8913  cflecard  9035  canth4  9429  canthnumlem  9430  canthwelem  9432  canthp1lem2  9435  pwfseqlem4  9444  wunex3  9523  addsrpr  9856  mulsrpr  9857  recexsrlem  9884  mulcani  10626  div1  10676  recdiv  10691  divdiv1  10696  divdiv2  10697  div23i  10743  div11i  10744  divmuldivi  10745  divadddivi  10747  divdivdivi  10748  lemulge11  10845  negiso  10963  dfnn3  10994  2cnne0  11202  2rene0  11203  halfpm6th  11213  avglt1  11230  avglt2  11231  div4p1lem1div2  11247  3halfnz  11416  divlt1lt  11859  divle1le  11860  nnledivrp  11900  x2times  12088  xrsupsslem  12096  xrinfmsslem  12097  fz0to4untppr  12399  fldiv4lem1div2uz2  12593  om2uzoi  12710  fzennn  12723  expge1  12853  sqoddm1div8  12984  faclbnd2  13034  faclbnd4lem1  13036  4bc2eq6  13072  hashfxnn0  13080  hashfOLD  13082  hashsnlei  13162  hashunlei  13168  hashsslei  13169  hash2prb  13208  repswccat  13485  cshwsexa  13523  funcnvs4  13612  f1oun2prg  13614  wrdlen2i  13636  relexpaddg  13743  cjreb  13813  sqrt2gt1lt2  13965  abs1m  14025  amgm2  14059  climcndslem2  14526  fprodn0f  14666  bpoly3  14733  efcllem  14752  ege2le3  14764  efi4p  14811  efival  14826  sin01bnd  14859  cos01bnd  14860  cos1bnd  14861  cos2bnd  14862  sin01gt0  14864  cos01gt0  14865  sin02gt0  14866  sincos2sgn  14868  sin4lt0  14869  egt2lt3  14878  rpnnen2lem3  14889  rpnnen2lem11  14897  nthruc  14924  nthruz  14925  3dvdsdec  14997  3dvdsdecOLD  14998  3dvds2dec  14999  3dvds2decOLD  15000  mod2eq1n2dvds  15014  oddge22np1  15016  halfleoddlt  15029  nno  15041  divalglem5  15063  ndvdsi  15079  flodddiv4  15080  flodddiv4lt  15082  flodddiv4t2lthalf  15083  bitsp1o  15098  3lcm2e6woprm  15271  6lcm4e12  15272  pcrec  15506  prmrec  15569  prmo1  15684  prmgaplcmlem1  15698  prmgaplcm  15707  modsubi  15719  structfn  15816  strlemor0OLD  15908  strlemor1OLD  15909  strleun  15912  isofn  16375  sscres  16423  funcestrcsetclem7  16726  funcestrcsetclem8  16727  fullestrcsetc  16731  mgmnsgrpex  17358  ga0  17671  symg2bas  17758  f1otrspeq  17807  psgnsn  17880  0frgp  18132  gsummptnn0fz  18322  srgbinomlem4  18483  psrbag0  19434  psrbagsn  19435  coe1fsupp  19524  coe1mul2  19579  evls1sca  19628  cnfldfun  19698  cnfldfunALT  19699  cnfld1  19711  cnsubdrglem  19737  expmhm  19755  expghm  19784  matmulr  20184  mat1dimelbas  20217  mat1f1o  20224  m2detleib  20377  smadiadetglem1  20417  pmatcollpw3fi1lem2  20532  cpmidpmatlem2  20616  cpmadumatpolylem1  20626  cayhamlem3  20632  cayhamlem4  20633  toprntopon  20669  isbasis3g  20693  fctop  20748  cctop  20750  refref  21256  bl2in  22145  dscmet  22317  iihalf1  22670  iihalf2  22672  icopnfhmeo  22682  iccpnfhmeo  22684  xrhmeo  22685  iscvsi  22869  zclmncvs  22888  ncvs1  22897  minveclem2  23137  minveclem4  23143  ovolunlem1a  23204  volf  23237  i1f1lem  23396  mbfi1fseqlem5  23426  dveflem  23680  pilem2  24144  pilem3  24145  sinhalfpilem  24153  sincosq1lem  24187  tangtx  24195  sinq12gt0  24197  sincos4thpi  24203  sincos6thpi  24205  sincos3rdpi  24206  pige3  24207  coseq1  24212  efeq1  24213  efif1olem4  24229  logblog  24464  angneg  24467  ang180lem1  24473  1cubrlem  24502  quart1  24517  log2cnv  24605  log2tlbnd  24606  log2ublem1  24607  log2ub  24610  emcllem1  24656  emcllem6  24661  basellem1  24741  basellem2  24742  basellem3  24743  basellem8  24748  ppiublem1  24861  ppiublem2  24862  ppiub  24863  chtublem  24870  chtub  24871  bcmono  24936  bclbnd  24939  bpos1lem  24941  bposlem1  24943  bposlem2  24944  bposlem3  24945  bposlem4  24946  bposlem5  24947  bposlem6  24948  bposlem7  24949  bposlem8  24950  bposlem9  24951  lgsdir2lem1  24984  1lgs  24999  gausslemma2dlem0c  25017  gausslemma2dlem0d  25018  gausslemma2dlem1a  25024  gausslemma2dlem2  25026  gausslemma2dlem3  25027  gausslemma2dlem5  25030  gausslemma2dlem6  25031  lgsquad2lem2  25044  2lgslem1a1  25048  2lgslem1a2  25049  2lgslem1c  25052  2lgslem3a  25055  2lgslem3b  25056  2lgslem3c  25057  2lgslem3d  25058  2lgslem3  25063  2lgsoddprmlem1  25067  chebbnd1lem1  25092  chebbnd1lem3  25094  chebbnd1  25095  dchrisum0flblem2  25132  dchrisum0lem1  25139  mulog2sumlem2  25158  selberglem2  25169  chpdifbndlem1  25176  ercgrg  25346  axlowdimlem4  25759  axlowdimlem5  25760  axlowdimlem6  25761  axlowdimlem7  25762  axlowdimlem8  25763  axlowdimlem10  25765  axlowdimlem11  25766  graop  25855  grastruct  25856  uhgrunop  25900  upgrunop  25943  umgrunop  25945  usgrop  25985  usgr2v1e2w  26071  usgrexmpldifpr  26077  usgrexmpledg  26081  uhgrsubgrself  26099  uhgrspan1lem1  26119  upgrres1lem1  26123  fusgrfis  26144  vtxd0nedgb  26304  p1evtxdeqlem  26328  p1evtxdeq  26329  p1evtxdp1  26330  umgr2v2e  26341  vdegp1bi  26353  wlkcomp  26430  upgr2pthnlp  26531  usgr2trlncl  26559  usgr2pthlem  26562  clwlkcomp  26578  uspgrn2crct  26603  wspthnonp  26647  2wlkond  26736  2pthond  26741  2pthon3v  26742  umgr2adedgwlkonALT  26746  umgr2wlk  26748  umgr2wlkon  26749  wpthswwlks2on  26756  elwspths2spth  26763  0ewlk  26875  0pth  26886  0pthonv  26890  1pthon2v  26913  3wlkdlem4  26922  3trlond  26933  3pthond  26935  3spthond  26937  trlsegvdeglem3  26982  eupthvdres  26995  eupth2lemb  26997  ex-natded5.2i  27151  ex-an  27167  ex-id  27179  ex-po  27180  ex-fl  27192  ex-mod  27194  ex-exp  27195  ex-lcm  27203  nvz0  27411  ipidsq  27453  ipdirilem  27572  siilem1  27594  minvecolem2  27619  minvecolem3  27620  minvecolem4  27624  hvsubcan  27819  hvsubcan2  27820  normlem7tALT  27864  helch  27988  hsn0elch  27993  hhshsslem2  28013  hhsssh  28014  shscli  28064  shintcli  28076  shintcl  28077  chintcli  28078  chintcl  28079  shincli  28109  shsval2i  28134  omlsi  28151  chincli  28207  chabs1  28263  fh1i  28368  fh2i  28369  cm2ji  28372  pjnormi  28468  nmopsetn0  28612  nmfnsetn0  28625  lnophm  28766  nmcexi  28773  nmbdfnlb  28797  imaelshi  28805  nlelshi  28807  nmopadjlem  28836  nmopcoadji  28848  hmopidmch  28900  hmopidmpj  28901  sto1i  28983  stlei  28987  stji1i  28989  csmdsymi  29081  chirred  29142  cdj3lem1  29181  xrsclat  29507  nn0archi  29670  lmatfvlem  29705  xrge0iifmhm  29809  qqh0  29852  qqh1  29853  rerrext  29877  cnrrext  29878  prsiga  30017  oms0  30182  coinfliprv  30367  ballotlem1  30371  ballotth  30422  signsw0g  30455  subfacval2  30930  erdszelem2  30935  cvmliftlem4  31031  elmrsubrn  31178  msubfval  31182  problem4  31323  quad3  31325  dfpo2  31406  br6  31408  dfon2lem3  31444  poseq  31504  fullfunfnv  31748  fneref  32040  filnetlem2  32069  filnetlem3  32070  onpsstopbas  32124  dnizeq0  32160  dnibndlem12  32174  knoppcnlem5  32182  knoppcnlem8  32185  knoppcnlem10  32187  knoppcnlem11  32188  knoppndvlem14  32211  cnndvlem1  32223  bj-genr  32286  bj-genl  32287  bj-genan  32288  bj-2upln1upl  32712  bj-vtoclgfALT  32721  taupilem1  32839  topdifinf  32868  sin2h  33070  cos2h  33071  tan2h  33072  pigt3  33073  poimirlem1  33081  poimirlem2  33082  poimirlem3  33083  poimirlem4  33084  poimirlem6  33086  poimirlem7  33087  poimirlem11  33091  poimirlem12  33092  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  poimirlem22  33102  poimirlem23  33103  poimirlem24  33104  poimirlem25  33105  poimirlem26  33106  poimirlem29  33109  poimirlem31  33111  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  itg2addnclem2  33133  asindmre  33166  heiborlem7  33287  riscer  33458  ac6s6f  33652  ishlatiN  34161  0psubN  34554  atpsubN  34558  mzpclall  36809  diophin  36855  diophun  36856  eldioph4b  36894  irrapx1  36911  2nn0ind  37029  aomclem4  37146  ifpid3g  37357  ifpid2g  37358  ifpbi1b  37368  pwinfi  37389  rtrclex  37444  cnvrcl0  37452  dfrcl2  37486  relexp1idm  37526  relexp0idm  37527  clsk1independent  37865  lhe4.4ex1a  38049  expgrowth  38055  ax6e2nd  38295  uun0.1  38526  relopabVD  38659  ax6e2ndVD  38666  sb5ALTVD  38671  ax6e2ndALT  38688  fnchoice  38710  limsuppnfdlem  39369  dvmptconst  39465  dvmptidg  39467  dvmulcncf  39477  dvdivcncf  39479  dvnprodlem3  39500  itgsinexplem1  39506  volioof  39541  stoweidlem13  39567  stoweidlem14  39568  stoweidlem26  39580  stoweidlem34  39588  stoweidlem49  39603  stoweidlem59  39613  dirkertrigeqlem3  39654  dirkercncflem1  39657  dirkercncflem2  39658  fourierdlem57  39717  fourierdlem62  39722  fourierdlem103  39763  fourierdlem111  39771  fourierswlem  39784  fouriersw  39785  salexct2  39894  salexct3  39897  salgencntex  39898  salgensscntex  39899  gsumge0cl  39925  sge00  39930  sge0tsms  39934  0ome  40080  ovnlecvr  40109  ovn0lem  40116  hoidmvle  40151  ovnsubadd2lem  40196  smflimlem6  40321  mbfpsssmf  40328  smfmullem4  40338  smfpimbor1lem1  40342  astbstanbst  40410  aistbistaandb  40411  abnotataxb  40417  aifftbifffaibif  40422  confun4  40443  plcofph  40445  plvcofph  40447  plvcofphax  40448  plvofpos  40449  mdandyv0  40450  mdandyv1  40451  mdandyv2  40452  mdandyv3  40453  mdandyv4  40454  mdandyv5  40455  mdandyv6  40456  mdandyv7  40457  mdandyv8  40458  mdandyv9  40459  mdandyv10  40460  mdandyv11  40461  mdandyv12  40462  mdandyv13  40463  mdandyv14  40464  mdandyv15  40465  mdandyvr0  40466  mdandyvr1  40467  mdandyvr2  40468  mdandyvr3  40469  mdandyvr4  40470  mdandyvr5  40471  mdandyvr6  40472  mdandyvr7  40473  mdandyvrx0  40482  mdandyvrx1  40483  mdandyvrx2  40484  mdandyvrx3  40485  mdandyvrx4  40486  mdandyvrx5  40487  mdandyvrx6  40488  mdandyvrx7  40489  dandysum2p2e4  40499  pfx2  40741  fmtno4prmfac  40813  31prm  40841  lighneallem4a  40854  41prothprmlem2  40864  zofldiv2ALTV  40903  gbegt5  40974  gbogt5  40975  gboage9  40977  9gboa  40987  11gboa  40988  nnsum3primes4  40995  nnsum3primesgbe  40999  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  tgblthelfgott  41020  tgoldbach  41023  tgblthelfgottOLD  41027  tgoldbachOLD  41030  mgmplusgiopALT  41148  sgrp2sgrp  41182  isrnghm  41210  2zrngaabl  41262  rnghmsscmap2  41291  rnghmsscmap  41292  funcrngcsetc  41316  funcrngcsetcALT  41317  rhmsscmap2  41337  rhmsscmap  41338  funcringcsetc  41353  funcringcsetcALTV2lem8  41361  funcringcsetclem8ALTV  41384  zlmodzxzlmod  41450  zlmodzxzel  41451  zlmodzxzscm  41453  zlmodzxzadd  41454  snlindsntorlem  41577  ldepspr  41580  lmod1lem2  41595  lmod1lem3  41596  lmod1lem4  41597  lmod1lem5  41598  lmodn0  41602  zlmodzxznm  41604  zlmodzxzldeplem  41605  zlmodzxzldeplem1  41607  zlmodzxzldeplem3  41609  lvecpsslmod  41614  ldepsnlinc  41615  ldepslinc  41616  expnegico01  41626  zofldiv2  41643  flnn0div2ge  41645  elbigo2  41668  nnlog2ge0lt1  41682  digfval  41713  dignnld  41719  dignn0flhalf  41734  dpfrac1  41836  dpfrac1OLD  41837  alimp-surprise  41859  aacllem  41880
  Copyright terms: Public domain W3C validator