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 458
Description: Infer conjunction of premises. Inference associated with pm3.2 457. Its associated deduction is jca 503 (and the double deduction is jcad 504). (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 457 . 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 198  df-an 385
This theorem is referenced by:  dfbi  463  mp4an  676  pm4.87  860  3pm3.2i  1431  unssi  3985  ssini  4030  bm1.3ii  4976  opthhausdorff  5170  epelg  5223  elvv  5375  relopabi  5445  funpr  6154  funcnvpr  6160  mpt2v  6978  caovcom  7059  snnex  7194  pwnex  7196  1st2val  7424  2nd2val  7425  elxp7  7431  mptmpt2opabbrd  7479  wfrlem13  7661  wfr3  7669  tfr1a  7724  oeoa  7912  oeoe  7914  erov  8078  endisj  8284  phplem2  8377  snopfsupp  8535  r1funlim  8874  dfac2b  9234  dfac2OLD  9236  cflecard  9358  canth4  9752  canthnumlem  9753  canthwelem  9755  canthp1lem2  9758  pwfseqlem4  9767  wunex3  9846  addsrpr  10179  mulsrpr  10180  recexsrlem  10207  mulcani  10949  div1  10999  recdiv  11014  divdiv1  11019  divdiv2  11020  div23i  11066  div11i  11067  divmuldivi  11068  divadddivi  11070  divdivdivi  11071  lemulge11  11168  negiso  11286  dfnn3  11317  2cnne0  11507  2rene0  11508  halfpm6th  11518  avglt1  11535  avglt2  11536  div4p1lem1div2  11552  3halfnz  11720  divlt1lt  12111  divle1le  12112  nnledivrp  12154  x2times  12345  xrsupsslem  12353  xrinfmsslem  12354  fz0to4untppr  12664  om2uzoi  12976  fzennn  12989  expge1  13118  sqoddm1div8  13249  faclbnd2  13296  faclbnd4lem1  13298  4bc2eq6  13334  hashfxnn0  13342  hashfOLD  13344  hashsnlei  13421  hashunlei  13427  hashsslei  13428  hash2prb  13469  repswccat  13754  cshwsexa  13792  funcnvs4  13882  f1oun2prg  13884  wrdlen2i  13909  relexpaddg  14014  cjreb  14084  sqrt2gt1lt2  14236  abs1m  14296  fprodn0f  14940  bpoly3  15007  ege2le3  15038  efi4p  15085  efival  15100  sin01bnd  15133  cos01bnd  15134  cos1bnd  15135  cos2bnd  15136  sin01gt0  15138  cos01gt0  15139  sin02gt0  15140  sincos2sgn  15142  sin4lt0  15143  egt2lt3  15152  rpnnen2lem3  15163  rpnnen2lem11  15171  nthruc  15199  nthruz  15200  3dvdsdec  15274  3dvds2dec  15275  mod2eq1n2dvds  15289  halfleoddlt  15304  divalglem5  15338  ndvdsi  15353  flodddiv4  15354  flodddiv4lt  15356  bitsp1o  15372  3lcm2e6woprm  15545  6lcm4e12  15546  pcrec  15778  prmrec  15841  prmo1  15956  prmgaplcmlem1  15970  prmgaplcm  15979  modsubi  15991  structfn  16083  strlemor0OLD  16177  strlemor1OLD  16178  strleun  16181  isofn  16637  sscres  16685  funcestrcsetclem7  16989  funcestrcsetclem8  16990  fullestrcsetc  16994  mgmnsgrpex  17621  ga0  17930  symg2bas  18017  f1otrspeq  18066  psgnsn  18139  0frgp  18391  gsummptnn0fz  18581  gsummptnn0fzOLD  18582  srgbinomlem4  18743  psrbag0  19700  psrbagsn  19701  coe1fsupp  19790  coe1mul2  19845  evls1sca  19894  cnfldfun  19964  cnfldfunALT  19965  cnfld1  19977  cnsubdrglem  20003  expmhm  20021  expghm  20050  matmulr  20452  mat1dimelbas  20486  mat1f1o  20493  m2detleib  20646  smadiadetglem1  20687  pmatcollpw3fi1lem2  20803  cpmidpmatlem2  20887  cpmadumatpolylem1  20897  cayhamlem3  20903  cayhamlem4  20904  toprntopon  20941  isbasis3g  20965  fctop  21020  cctop  21022  refref  21528  bl2in  22416  dscmet  22588  iihalf1  22941  iihalf2  22943  icopnfhmeo  22953  iccpnfhmeo  22955  xrhmeo  22956  iscvsi  23139  zclmncvs  23158  ncvs1  23167  minveclem2  23407  minveclem4  23413  ovolunlem1a  23475  volf  23508  i1f1lem  23668  mbfi1fseqlem5  23698  dveflem  23954  pilem2  24418  pilem3  24419  pilem3OLD  24420  sinhalfpilem  24428  sincosq1lem  24462  tangtx  24470  sinq12gt0  24472  sincos4thpi  24478  sincos6thpi  24480  sincos3rdpi  24481  pige3  24482  coseq1  24487  efeq1  24488  efif1olem4  24504  logblog  24742  angneg  24745  ang180lem1  24751  1cubrlem  24780  quart1  24795  log2cnv  24883  log2tlbnd  24884  log2ublem1  24885  log2ub  24888  emcllem1  24934  emcllem6  24939  basellem1  25019  basellem2  25020  basellem3  25021  basellem8  25026  ppiublem1  25139  ppiublem2  25140  ppiub  25141  chtublem  25148  chtub  25149  bcmono  25214  bclbnd  25217  bpos1lem  25219  bposlem1  25221  bposlem2  25222  bposlem3  25223  bposlem4  25224  bposlem5  25225  bposlem6  25226  bposlem7  25227  bposlem8  25228  bposlem9  25229  lgsdir2lem1  25262  1lgs  25277  gausslemma2dlem0c  25295  gausslemma2dlem0d  25296  gausslemma2dlem1a  25302  gausslemma2dlem2  25304  gausslemma2dlem3  25305  gausslemma2dlem5  25308  gausslemma2dlem6  25309  lgsquad2lem2  25322  2lgslem1a1  25326  2lgslem1a2  25327  2lgslem1c  25330  2lgslem3a  25333  2lgslem3b  25334  2lgslem3c  25335  2lgslem3d  25336  2lgslem3  25341  2lgsoddprmlem1  25345  chebbnd1lem1  25370  chebbnd1lem3  25372  chebbnd1  25373  dchrisum0flblem2  25410  dchrisum0lem1  25417  mulog2sumlem2  25436  selberglem2  25447  chpdifbndlem1  25454  ercgrg  25624  axlowdimlem4  26037  axlowdimlem5  26038  axlowdimlem6  26039  axlowdimlem7  26040  axlowdimlem8  26041  axlowdimlem10  26043  axlowdimlem11  26044  graop  26133  grastruct  26134  uhgrunop  26182  upgrop  26201  upgrunop  26226  umgrunop  26228  usgrop  26271  usgr2v1e2w  26358  usgrexmpldifpr  26364  usgrexmpledg  26368  uhgrsubgrself  26386  uhgrspan1lem1  26406  upgrres1lem1  26415  fusgrfis  26436  vtxd0nedgb  26610  p1evtxdeqlem  26634  p1evtxdeq  26635  p1evtxdp1  26636  umgr2v2e  26647  vdegp1bi  26659  wlkcomp  26752  upgr2pthnlp  26854  usgr2trlncl  26882  usgr2pthlem  26885  clwlkcomp  26901  uspgrn2crct  26927  wwlksonvtx  26976  wspthnonp  26984  2wlkond  27075  2pthond  27080  2pthon3v  27081  umgr2adedgwlkonALT  27085  umgr2wlk  27087  umgr2wlkon  27088  wpthswwlks2on  27100  wpthswwlks2onOLD  27101  elwspths2spth  27107  0ewlk  27285  0pth  27296  0pthonv  27300  1pthon2v  27324  3wlkdlem4  27333  3trlond  27344  3pthond  27346  3spthond  27348  trlsegvdeglem3  27393  eupthvdres  27406  eupth2lemb  27408  ex-natded5.2i  27592  ex-an  27608  ex-id  27620  ex-po  27621  ex-fl  27633  ex-mod  27635  ex-exp  27636  ex-lcm  27644  nvz0  27849  ipidsq  27891  ipdirilem  28010  siilem1  28032  minvecolem2  28057  minvecolem3  28058  minvecolem4  28062  hvsubcan  28257  hvsubcan2  28258  normlem7tALT  28302  helch  28426  hsn0elch  28431  hhshsslem2  28451  hhsssh  28452  shscli  28502  shintcli  28514  shintcl  28515  chintcli  28516  chintcl  28517  shincli  28547  shsval2i  28572  omlsi  28589  chincli  28645  chabs1  28701  fh1i  28806  fh2i  28807  cm2ji  28810  pjnormi  28906  nmopsetn0  29050  nmfnsetn0  29063  lnophm  29204  nmcexi  29211  nmbdfnlb  29235  imaelshi  29243  nlelshi  29245  nmopadjlem  29274  nmopcoadji  29286  hmopidmch  29338  hmopidmpj  29339  sto1i  29421  stlei  29425  stji1i  29427  csmdsymi  29519  chirred  29580  cdj3lem1  29619  rpdp2cl  29913  dp2lt10  29915  dp2lt  29916  dp2ltc  29918  dpfrac1  29923  dplti  29936  dpgti  29937  dpexpp1  29939  dpadd3  29943  dpmul  29944  dpmul4  29945  xrsclat  30003  nn0archi  30166  lmatfvlem  30204  xrge0iifmhm  30308  qqh0  30351  qqh1  30352  rerrext  30376  cnrrext  30377  prsiga  30517  oms0  30682  coinfliprv  30867  ballotlem1  30871  ballotth  30922  signsw0g  30956  hgt750lemd  31049  hgt750lem  31052  hgt750lem2  31053  hgt750leme  31059  tgoldbachgt  31064  subfacval2  31490  erdszelem2  31495  cvmliftlem4  31591  elmrsubrn  31738  msubfval  31742  problem4  31882  quad3  31884  dfpo2  31965  br6  31967  dfon2lem3  32008  poseq  32072  fullfunfnv  32372  fneref  32664  filnetlem2  32693  filnetlem3  32694  onpsstopbas  32744  dnizeq0  32780  dnibndlem12  32794  knoppcnlem5  32802  knoppcnlem8  32805  knoppcnlem10  32807  knoppcnlem11  32808  knoppndvlem14  32831  cnndvlem1  32843  bj-genr  32904  bj-genl  32905  bj-genan  32906  bj-2upln1upl  33320  bj-vtoclgfALT  33329  taupilem1  33482  topdifinf  33511  sin2h  33710  cos2h  33711  tan2h  33712  pigt3  33713  poimirlem1  33721  poimirlem2  33722  poimirlem3  33723  poimirlem4  33724  poimirlem6  33726  poimirlem7  33727  poimirlem11  33731  poimirlem12  33732  poimirlem16  33736  poimirlem17  33737  poimirlem19  33739  poimirlem20  33740  poimirlem22  33742  poimirlem23  33743  poimirlem24  33744  poimirlem25  33745  poimirlem26  33746  poimirlem29  33749  poimirlem31  33751  mblfinlem3  33759  mblfinlem4  33760  ismblfin  33761  itg2addnclem2  33772  asindmre  33805  heiborlem7  33925  riscer  34096  ac6s6f  34289  refrelcoss3  34524  symrelcoss3  34526  ishlatiN  35133  0psubN  35527  atpsubN  35531  mzpclall  37790  diophin  37836  diophun  37837  eldioph4b  37875  irrapx1  37892  2nn0ind  38009  aomclem4  38126  ifpid3g  38335  ifpid2g  38336  ifpbi1b  38346  pwinfi  38367  rtrclex  38422  cnvrcl0  38430  dfrcl2  38464  relexp1idm  38504  relexp0idm  38505  clsk1independent  38842  lhe4.4ex1a  39026  expgrowth  39032  ax6e2nd  39270  uun0.1  39500  relopabVD  39629  ax6e2ndVD  39636  sb5ALTVD  39641  ax6e2ndALT  39658  fnchoice  39680  limsuppnfdlem  40411  dvmptconst  40607  dvmptidg  40609  dvmulcncf  40618  dvdivcncf  40620  dvnprodlem3  40641  itgsinexplem1  40647  volioof  40681  stoweidlem13  40707  stoweidlem14  40708  stoweidlem26  40720  stoweidlem34  40728  stoweidlem49  40743  stoweidlem59  40753  dirkertrigeqlem3  40794  dirkercncflem1  40797  dirkercncflem2  40798  fourierdlem57  40857  fourierdlem62  40862  fourierdlem103  40903  fourierdlem111  40911  fourierswlem  40924  fouriersw  40925  salexct2  41034  salexct3  41037  salgencntex  41038  salgensscntex  41039  gsumge0cl  41065  sge00  41070  sge0tsms  41074  0ome  41223  ovnlecvr  41252  ovn0lem  41259  hoidmvle  41294  ovnsubadd2lem  41339  smflimlem6  41464  mbfpsssmf  41471  smfmullem4  41481  smfpimbor1lem1  41485  astbstanbst  41556  aistbistaandb  41557  abnotataxb  41563  aifftbifffaibif  41568  confun4  41589  plcofph  41591  plvcofph  41593  plvcofphax  41594  plvofpos  41595  mdandyv0  41596  mdandyv1  41597  mdandyv2  41598  mdandyv3  41599  mdandyv4  41600  mdandyv5  41601  mdandyv6  41602  mdandyv7  41603  mdandyv8  41604  mdandyv9  41605  mdandyv10  41606  mdandyv11  41607  mdandyv12  41608  mdandyv13  41609  mdandyv14  41610  mdandyv15  41611  mdandyvr0  41612  mdandyvr1  41613  mdandyvr2  41614  mdandyvr3  41615  mdandyvr4  41616  mdandyvr5  41617  mdandyvr6  41618  mdandyvr7  41619  mdandyvrx0  41628  mdandyvrx1  41629  mdandyvrx2  41630  mdandyvrx3  41631  mdandyvrx4  41632  mdandyvrx5  41633  mdandyvrx6  41634  mdandyvrx7  41635  dandysum2p2e4  41645  dfnelbr2  41860  pfx2  41985  fmtno4prmfac  42057  31prm  42085  lighneallem4a  42098  41prothprmlem2  42108  zofldiv2ALTV  42147  gbegt5  42222  gbowgt5  42223  gboge9  42225  9gbo  42235  11gbo  42236  nnsum3primes4  42249  nnsum3primesgbe  42253  nnsum4primesodd  42257  nnsum4primesoddALTV  42258  nnsum4primeseven  42261  nnsum4primesevenALTV  42262  tgblthelfgott  42276  tgoldbach  42278  mgmplusgiopALT  42396  sgrp2sgrp  42430  isrnghm  42458  2zrngaabl  42510  rnghmsscmap2  42539  rnghmsscmap  42540  funcrngcsetc  42564  funcrngcsetcALT  42565  rhmsscmap2  42585  rhmsscmap  42586  funcringcsetc  42601  funcringcsetcALTV2lem8  42609  funcringcsetclem8ALTV  42632  zlmodzxzlmod  42698  zlmodzxzel  42699  zlmodzxzscm  42701  zlmodzxzadd  42702  snlindsntorlem  42825  ldepspr  42828  lmod1lem2  42843  lmod1lem3  42844  lmod1lem4  42845  lmod1lem5  42846  lmodn0  42850  zlmodzxznm  42852  zlmodzxzldeplem  42853  zlmodzxzldeplem1  42855  zlmodzxzldeplem3  42857  lvecpsslmod  42862  ldepsnlinc  42863  ldepslinc  42864  expnegico01  42874  zofldiv2  42891  flnn0div2ge  42893  elbigo2  42912  nnlog2ge0lt1  42926  digfval  42957  dignnld  42963  dignn0flhalf  42978  alimp-surprise  43095  aacllem  43116
  Copyright terms: Public domain W3C validator