Theorem pm3.2i 470

Description: Infer conjunction of premises. Inference associated with pm3.2 469. Its associated deduction is jca 511 (and the double deduction is jcad 512). (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

Step	Hyp	Ref	Expression
1		pm3.2i.1	. 2 ⊢ 𝜑
2		pm3.2i.2	. 2 ⊢ 𝜓
3		pm3.2 469	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 395

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

This theorem is referenced by:  mp4an  693  pm4.87  844  3pm3.2i  1340  unssi  4191  ssini  4240  opthhausdorff  5522  elvv  5760  elopaelxp  5775  relopabiv  5830  relopabi  5832  dfpo2  6316  funpr  6622  funcnvpr  6628  mpov  7545  caovcom  7630  snnex  7778  pwnex  7779  1st2val  8042  2nd2val  8043  elxp7  8049  opreuopreu  8059  mptmpoopabbrdOLDOLD  8108  poxp2  8168  poseq  8183  wfrlem13OLD  8361  wfr3OLD  8378  tfr1a  8434  oeoa  8635  oeoe  8637  erov  8854  endisj  9098  phplem2OLD  9255  snopfsupp  9431  ssttrcl  9755  ttrclselem2  9766  r1funlim  9806  dfac2b  10171  cflecard  10293  canth4  10687  canthnumlem  10688  canthwelem  10690  canthp1lem2  10693  pwfseqlem4  10702  wunex3  10781  addsrpr  11115  mulsrpr  11116  recexsrlem  11143  mulcani  11902  div1  11957  recdiv  11973  divdiv1  11978  divdiv2  11979  div23i  12025  div11i  12026  divmuldivi  12027  divadddivi  12029  divdivdivi  12030  lemulge11  12130  negiso  12248  dfnn3  12280  2cnne0  12476  2rene0  12477  halfpm6th  12487  avglt1  12504  avglt2  12505  div4p1lem1div2  12521  3halfnz  12697  divlt1lt  13104  divle1le  13105  nnledivrp  13147  x2times  13341  xrsupsslem  13349  xrinfmsslem  13350  fvf1tp  13829  om2uzoi  13996  fzennn  14009  expge1  14140  sqoddm1div8  14282  faclbnd2  14330  faclbnd4lem1  14332  4bc2eq6  14368  hashfxnn0  14376  hashsnlei  14457  hashunlei  14464  hashsslei  14465  hash2prb  14511  repswccat  14824  cshwsexaOLD  14863  funcnvs4  14954  f1oun2prg  14956  wrdlen2i  14981  s2rn  15002  s3rn  15003  s7rn  15004  relexpaddg  15092  cjreb  15162  sqrt2gt1lt2  15313  abs1m  15374  bpoly3  16094  ege2le3  16126  efi4p  16173  efival  16188  sin01bnd  16221  cos01bnd  16222  cos1bnd  16223  cos2bnd  16224  sin01gt0  16226  cos01gt0  16227  sin02gt0  16228  sincos2sgn  16230  sin4lt0  16231  egt2lt3  16242  rpnnen2lem3  16252  rpnnen2lem11  16260  nthruc  16288  nthruz  16289  3dvdsdec  16369  3dvds2dec  16370  mod2eq1n2dvds  16384  halfleoddlt  16399  divalglem5  16434  ndvdsi  16449  flodddiv4  16452  flodddiv4lt  16454  bitsp1o  16470  3lcm2e6woprm  16652  6lcm4e12  16653  pcrec  16896  prmrec  16960  prmgaplcmlem1  17089  prmgaplcm  17098  modsubi  17110  structfn  17193  strleun  17194  slotsdifipndx  17379  slotsdifplendx  17419  slotsdifdsndx  17438  slotsdifunifndx  17445  slotsdifplendx2  17461  slotsdifocndx  17462  isofn  17819  sscres  17867  funcestrcsetclem7  18191  funcestrcsetclem8  18192  fullestrcsetc  18196  mgmnsgrpex  18944  pwmnd  18950  ga0  19316  symg2bas  19410  f1otrspeq  19465  psgnsn  19538  0frgp  19797  gsummptnn0fz  20004  srgbinomlem4  20226  isrnghm  20441  rnghmsscmap2  20629  rnghmsscmap  20630  funcrngcsetc  20640  funcrngcsetcALT  20641  rhmsscmap2  20658  rhmsscmap  20659  funcringcsetc  20674  cnfldfun  21378  cnfldfunALT  21379  cnfldfunOLD  21391  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  cnfld1  21406  cnfld1OLD  21407  cnsubdrglem  21436  expmhm  21454  expghm  21486  pzriprnglem4  21495  pzriprnglem9  21500  pzriprnglem14  21505  pzriprng1ALT  21507  psrbag0  22086  psrbagsn  22087  coe1fsupp  22216  coe1mul2  22272  evls1sca  22327  matmulr  22444  mat1dimelbas  22477  mat1f1o  22484  m2detleib  22637  smadiadetglem1  22677  pmatcollpw3fi1lem2  22793  cpmidpmatlem2  22877  cpmadumatpolylem1  22887  cayhamlem3  22893  cayhamlem4  22894  isbasis3g  22956  fctop  23011  cctop  23013  refref  23521  bl2in  24410  dscmet  24585  iihalf1  24958  iihalf2  24961  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  iscvsi  25162  zclmncvs  25182  ncvs1  25191  ehl2eudis  25456  minveclem2  25460  minveclem4  25466  ovolunlem1a  25531  volf  25564  i1f1lem  25724  mbfi1fseqlem5  25754  dveflem  26017  pilem2  26496  pilem3  26497  sinhalfpilem  26505  sincosq1lem  26539  tangtx  26547  sinq12gt0  26549  sincos4thpi  26555  sincos6thpi  26558  sincos3rdpi  26559  pigt3  26560  pige3ALT  26562  coseq1  26567  efeq1  26570  efif1olem4  26587  angneg  26846  ang180lem1  26852  1cubrlem  26884  quart1  26899  log2cnv  26987  log2tlbnd  26988  log2ublem1  26989  log2ub  26992  emcllem1  27039  emcllem6  27044  basellem1  27124  basellem2  27125  basellem3  27126  basellem8  27131  ppiublem1  27246  ppiublem2  27247  ppiub  27248  chtublem  27255  chtub  27256  bcmono  27321  bclbnd  27324  bpos1lem  27326  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem7  27334  bposlem8  27335  bposlem9  27336  lgsdir2lem1  27369  1lgs  27384  gausslemma2dlem0c  27402  gausslemma2dlem0d  27403  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem3  27412  gausslemma2dlem5  27415  gausslemma2dlem6  27416  lgsquad2lem2  27429  2lgslem1a1  27433  2lgslem1a2  27434  2lgslem1c  27437  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgslem3  27448  2lgsoddprmlem1  27452  addsqrexnreu  27486  addsqnreup  27487  chebbnd1lem1  27513  chebbnd1lem3  27515  chebbnd1  27516  dchrisum0flblem2  27553  dchrisum0lem1  27560  mulog2sumlem2  27579  selberglem2  27590  chpdifbndlem1  27597  mulscl  28160  sltmul  28162  divs1  28229  precsexlem8  28238  nohalf  28407  0reno  28429  slotsinbpsd  28449  slotslnbpsd  28450  ercgrg  28525  axlowdimlem4  28960  axlowdimlem5  28961  axlowdimlem6  28962  axlowdimlem7  28963  axlowdimlem8  28964  axlowdimlem10  28966  axlowdimlem11  28967  graop  29046  grastruct  29047  uhgrunop  29092  upgrop  29111  upgrunop  29136  umgrunop  29138  usgrop  29180  usgr2v1e2w  29269  usgrexmpldifpr  29275  usgrexmpledg  29279  uhgrsubgrself  29297  uhgrspan1lem1  29317  upgrres1lem1  29326  fusgrfis  29347  vtxd0nedgb  29506  p1evtxdeqlem  29530  p1evtxdeq  29531  p1evtxdp1  29532  umgr2v2e  29543  vdegp1bi  29555  wlkcomp  29649  upgr2pthnlp  29752  usgr2trlncl  29780  usgr2pthlem  29783  clwlkcomp  29799  uspgrn2crct  29828  wwlksonvtx  29875  wspthnonp  29879  2wlkond  29957  2pthond  29962  2pthon3v  29963  umgr2adedgwlkonALT  29967  umgr2wlk  29969  umgr2wlkon  29970  wpthswwlks2on  29981  elwspths2spth  29987  0ewlk  30133  0pth  30144  0pthonv  30148  1pthon2v  30172  3wlkdlem4  30181  3trlond  30192  3pthond  30194  3spthond  30196  trlsegvdeglem3  30241  eupthvdres  30254  eupth2lemb  30256  ex-natded5.2i  30425  ex-an  30441  ex-id  30453  ex-po  30454  ex-fl  30466  ex-mod  30468  ex-exp  30469  ex-lcm  30477  nvz0  30687  ipidsq  30729  ipdirilem  30848  siilem1  30870  minvecolem2  30894  minvecolem3  30895  minvecolem4  30899  hvsubcan  31093  hvsubcan2  31094  normlem7tALT  31138  helch  31262  hsn0elch  31267  hhshsslem2  31287  hhsssh  31288  shscli  31336  shintcli  31348  shintcl  31349  chintcli  31350  chintcl  31351  shincli  31381  shsval2i  31406  omlsi  31423  chincli  31479  chabs1  31535  fh1i  31640  fh2i  31641  cm2ji  31644  pjnormi  31740  nmopsetn0  31884  nmfnsetn0  31897  lnophm  32038  nmcexi  32045  nmbdfnlb  32069  imaelshi  32077  nlelshi  32079  nmopadjlem  32108  nmopcoadji  32120  hmopidmch  32172  hmopidmpj  32173  sto1i  32255  stlei  32259  stji1i  32261  csmdsymi  32353  chirred  32414  cdj3lem1  32453  rpdp2cl  32864  dp2lt10  32866  dp2lt  32867  dp2ltc  32869  dpfrac1  32874  dplti  32887  dpgti  32888  dpexpp1  32890  dpadd3  32894  dpmul  32895  dpmul4  32896  xrsclat  33013  nn0archi  33375  zringfrac  33582  lmatfvlem  33814  xrge0iifmhm  33938  qqh0  33985  qqh1  33986  rerrext  34010  cnrrext  34011  prsiga  34132  oms0  34299  coinfliprv  34485  ballotlem1  34489  ballotth  34540  signsw0g  34571  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  hgt750leme  34673  tgoldbachgt  34678  subfacval2  35192  erdszelem2  35197  cvmliftlem4  35293  satom  35361  satfv1  35368  sat1el2xp  35384  fmlaomn0  35395  satfdmfmla  35405  satfv1fvfmla1  35428  ex-sategoelelomsuc  35431  ex-sategoelel12  35432  prv0  35435  prv1n  35436  elmrsubrn  35525  msubfval  35529  problem4  35673  quad3  35675  br6  35757  dfon2lem3  35786  fullfunfnv  35947  itgeq12i  36207  fneref  36351  filnetlem2  36380  filnetlem3  36381  onpsstopbas  36431  dnizeq0  36476  dnibndlem12  36490  knoppcnlem5  36498  knoppcnlem8  36501  knoppcnlem11  36504  knoppndvlem14  36526  cnndvlem1  36538  bj-genr  36607  bj-genl  36608  bj-genan  36609  bj-2upln1upl  37025  bj-vtoclgfALT  37060  bj-brab2a1  37150  bj-opabssvv  37151  taupilem1  37322  topdifinf  37350  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem29  37656  poimirlem31  37658  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem2  37679  asindmre  37710  heiborlem7  37824  riscer  37995  refrelcoss3  38464  symrelcoss3  38466  ishlatiN  39356  0psubN  39751  atpsubN  39755  gcdcomnni  41989  gcdnegnni  41990  neggcdnni  41991  60gcd7e1  42006  lcmeprodgcdi  42008  lcm2un  42015  lcm3un  42016  lcmineqlem4  42033  lcmineqlem6  42035  3lexlogpow5ineq1  42055  aks4d1p1p2  42071  mzpclall  42738  diophin  42783  diophun  42784  eldioph4b  42822  irrapx1  42839  2nn0ind  42957  aomclem4  43069  onexlimgt  43255  nnoeomeqom  43325  oaomoencom  43330  oenassex  43331  succlg  43341  dflim5  43342  omabs2  43345  tfsconcatfv2  43353  ifpid3g  43505  ifpid2g  43506  ifpbi1b  43516  eu0  43533  pwinfi  43577  rtrclex  43630  cnvrcl0  43638  dfrcl2  43687  relexp1idm  43727  relexp0idm  43728  clsk1independent  44059  lhe4.4ex1a  44348  expgrowth  44354  ax6e2nd  44578  uun0.1  44798  relopabVD  44921  ax6e2ndVD  44928  sb5ALTVD  44933  ax6e2ndALT  44950  rexanuz2nf  45503  dvmptconst  45930  dvmptidg  45932  dvmulcncf  45940  dvdivcncf  45942  dvnprodlem3  45963  itgsinexplem1  45969  volioof  46002  stoweidlem13  46028  stoweidlem14  46029  stoweidlem26  46041  stoweidlem34  46049  stoweidlem49  46064  stoweidlem59  46074  dirkertrigeqlem3  46115  dirkercncflem1  46118  dirkercncflem2  46119  fourierdlem57  46178  fourierdlem62  46183  fourierdlem103  46224  fourierdlem111  46232  fourierswlem  46245  fouriersw  46246  salexct2  46354  salexct3  46357  salgencntex  46358  salgensscntex  46359  gsumge0cl  46386  sge00  46391  sge0tsms  46395  0ome  46544  ovnlecvr  46573  ovn0lem  46580  hoidmvle  46615  ovnsubadd2lem  46660  smflimlem6  46791  mbfpsssmf  46798  smfmullem4  46809  smfpimbor1lem1  46813  astbstanbst  46921  aistbistaandb  46922  abnotataxb  46928  aifftbifffaibif  46933  confun4  46954  plcofph  46956  plvcofph  46958  plvcofphax  46959  plvofpos  46960  mdandyv0  46961  mdandyv1  46962  mdandyv2  46963  mdandyv3  46964  mdandyv4  46965  mdandyv5  46966  mdandyv6  46967  mdandyv7  46968  mdandyv8  46969  mdandyv9  46970  mdandyv10  46971  mdandyv11  46972  mdandyv12  46973  mdandyv13  46974  mdandyv14  46975  mdandyv15  46976  mdandyvr0  46977  mdandyvr1  46978  mdandyvr2  46979  mdandyvr3  46980  mdandyvr4  46981  mdandyvr5  46982  mdandyvr6  46983  mdandyvr7  46984  mdandyvrx0  46993  mdandyvrx1  46994  mdandyvrx2  46995  mdandyvrx3  46996  mdandyvrx4  46997  mdandyvrx5  46998  mdandyvrx6  46999  mdandyvrx7  47000  dandysum2p2e4  47010  or2expropbilem1  47044  dfnelbr2  47285  ich2exprop  47458  paireqne  47498  fmtno4prmfac  47559  31prm  47584  lighneallem4a  47595  41prothprmlem2  47605  zofldiv2ALTV  47649  nfermltl8rev  47729  nfermltl2rev  47730  nfermltlrev  47731  gbegt5  47748  gbowgt5  47749  gboge9  47751  9gbo  47761  11gbo  47762  nnsum3primes4  47775  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  tgblthelfgott  47802  tgoldbach  47804  ushggricedg  47896  isubgrgrim  47897  stgrvtx  47921  stgriedg  47922  stgrusgra  47926  stgr1  47928  uspgrlim  47959  clnbgr3stgrgrlic  47979  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  gpgvtx  48002  gpgiedg  48003  gpgorder  48013  2ltceilhalf  48015  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg3kgrtriexlem3  48041  gpg3kgrtriexlem6  48044  nn0mnd  48095  mgmplusgiopALT  48110  sgrp2sgrp  48144  2zrngaabl  48166  funcringcsetcALTV2lem8  48213  funcringcsetclem8ALTV  48236  zlmodzxzlmod  48270  zlmodzxzel  48271  zlmodzxzscm  48273  zlmodzxzadd  48274  snlindsntorlem  48387  ldepspr  48390  lmod1lem2  48405  lmod1lem3  48406  lmod1lem4  48407  lmod1lem5  48408  lmodn0  48412  zlmodzxznm  48414  zlmodzxzldeplem  48415  zlmodzxzldeplem1  48417  zlmodzxzldeplem3  48419  lvecpsslmod  48424  ldepsnlinc  48425  ldepslinc  48426  expnegico01  48435  zofldiv2  48452  flnn0div2ge  48454  elbigo2  48473  nnlog2ge0lt1  48487  digfval  48518  dignnld  48524  dignn0flhalf  48539  2arymaptfo  48575  itcovalt2lem1  48596  prelrrx2  48634  eenglngeehlnmlem2  48659  rrxsphere  48669  line2  48673  line2x  48675  line2y  48676  itsclc0yqsollem2  48684  inlinecirc02plem  48707  sepfsepc  48825  alimp-surprise  49299  aacllem  49320