Theorem pm3.2i 475

Description: Infer conjunction of premises. Inference associated with pm3.2 474. Its associated deduction is jca 520 (and the double deduction is jcad 521). (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 474	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mp4an  705  pm4.87  856  3pm3.2i  1356  sbt  2098  unssi  4146  ssini  4194  opthhausdorff  5490  elvv  5726  elopaelxp  5741  relopabiv  5797  relopabi  5799  dfpo2  6286  funpr  6581  funcnvpr  6587  mpov  7512  caovcom  7597  snnex  7745  pwnex  7746  1st2val  8002  2nd2val  8003  elxp7  8009  opreuopreu  8019  poxp2  8127  poseq  8142  tfr1a  8369  oeoa  8571  oeoe  8573  erov  8800  endisj  9040  snopfsupp  9339  ssttrcl  9672  ttrclselem2  9683  r1funlim  9726  dfac2b  10102  cflecard  10224  canth4  10620  canthnumlem  10621  canthwelem  10623  canthp1lem2  10626  pwfseqlem4  10635  wunex3  10714  addsrpr  11048  mulsrpr  11049  recexsrlem  11076  mulcani  11841  div1  11892  recdiv  11909  divdiv1  11914  divdiv2  11915  div23i  11961  div11i  11962  divmuldivi  11963  divadddivi  11965  divdivdivi  11966  lemulge11  12065  negiso  12183  dfnn3  12235  2cnne0  12441  2rene0  12442  halfpm6th  12454  avglt1  12470  avglt2  12471  div4p1lem1div2  12487  3halfnz  12663  divlt1lt  13075  divle1le  13076  nnledivrp  13118  x2times  13313  xrsupsslem  13321  xrinfmsslem  13322  nnge2recico01  13522  fvf1tp  13810  om2uzoi  13979  fzennn  13992  expge1  14123  sqoddm1div8  14267  faclbnd2  14315  faclbnd4lem1  14317  4bc2eq6  14353  hashfxnn0  14361  hashsnlei  14443  hashunlei  14450  hashsslei  14451  hash2prb  14497  repswccat  14811  funcnvs4  14940  f1oun2prg  14942  wrdlen2i  14967  s2rn  14988  s3rn  14989  s7rn  14990  relexpaddg  15078  cjreb  15162  sqrt2gt1lt2  15313  abs1m  15375  bpoly3  16100  ege2le3  16132  efi4p  16181  efival  16196  sin01bnd  16229  cos01bnd  16230  cos1bnd  16231  cos2bnd  16232  sin01gt0  16234  cos01gt0  16235  sin02gt0  16236  sincos2sgn  16238  sin4lt0  16239  egt2lt3  16250  rpnnen2lem3  16260  rpnnen2lem11  16268  nthruc  16296  nthruz  16297  3dvdsdec  16378  3dvds2dec  16379  mod2eq1n2dvds  16393  halfleoddlt  16408  divalglem5  16443  ndvdsi  16458  flodddiv4  16461  flodddiv4lt  16463  bitsp1o  16479  3lcm2e6woprm  16661  6lcm4e12  16662  pcrec  16906  prmrec  16970  prmgaplcmlem1  17099  prmgaplcm  17108  modsubi  17120  structfn  17204  strleun  17205  slotsdifipndx  17376  slotsdifplendx  17416  slotsdifdsndx  17435  slotsdifunifndx  17442  slotsdifplendx2  17457  slotsdifocndx  17458  isofn  17820  sscres  17868  funcestrcsetclem7  18190  funcestrcsetclem8  18191  fullestrcsetc  18195  nulchn  18663  chninf  18679  mgmnsgrpex  18981  pwmnd  18987  ga0  19356  symg2bas  19451  f1otrspeq  19505  psgnsn  19578  0frgp  19837  gsummptnn0fz  20044  srgbinomlem4  20299  isrnghm  20511  rnghmsscmap2  20702  rnghmsscmap  20703  funcrngcsetc  20713  funcrngcsetcALT  20714  rhmsscmap2  20731  rhmsscmap  20732  funcringcsetc  20747  cnfldfun  21493  cnfldfunALT  21494  cnfld1  21504  cnsubdrglem  21525  expmhm  21543  expghm  21582  pzriprnglem4  21591  pzriprnglem9  21596  pzriprnglem14  21601  pzriprng1ALT  21603  psrbag0  22170  psrbagsn  22171  coe1fsupp  22331  coe1mul2  22387  evls1sca  22440  matmulr  22552  mat1dimelbas  22585  mat1f1o  22592  m2detleib  22745  smadiadetglem1  22785  pmatcollpw3fi1lem2  22901  cpmidpmatlem2  22985  cpmadumatpolylem1  22995  cayhamlem3  23001  cayhamlem4  23002  isbasis3g  23063  fctop  23118  cctop  23120  refref  23627  bl2in  24514  dscmet  24686  iihalf1  25047  iihalf2  25049  icopnfhmeo  25059  iccpnfhmeo  25061  xrhmeo  25062  iscvsi  25245  zclmncvs  25264  ncvs1  25273  ehl2eudis  25538  minveclem2  25542  minveclem4  25548  ovolunlem1a  25612  volf  25645  i1f1lem  25805  mbfi1fseqlem5  25835  dveflem  26095  pilem2  26569  pilem3  26570  sinhalfpilem  26582  sincosq1lem  26616  tangtx  26624  sinq12gt0  26626  sincos4thpi  26632  sincos6thpi  26635  sincos3rdpi  26636  pigt3  26637  pige3ALT  26639  coseq1  26644  efeq1  26647  efif1olem4  26664  angneg  26922  ang180lem1  26928  1cubrlem  26960  quart1  26975  log2cnv  27063  log2tlbnd  27064  log2ublem1  27065  log2ub  27068  emcllem1  27114  emcllem6  27119  basellem1  27199  basellem2  27200  basellem3  27201  basellem8  27206  ppiublem1  27320  ppiublem2  27321  ppiub  27322  chtublem  27329  chtub  27330  bcmono  27395  bclbnd  27398  bpos1lem  27400  bposlem1  27402  bposlem2  27403  bposlem3  27404  bposlem4  27405  bposlem5  27406  bposlem6  27407  bposlem7  27408  bposlem8  27409  bposlem9  27410  lgsdir2lem1  27443  1lgs  27458  gausslemma2dlem0c  27476  gausslemma2dlem0d  27477  gausslemma2dlem1a  27483  gausslemma2dlem2  27485  gausslemma2dlem3  27486  gausslemma2dlem5  27489  gausslemma2dlem6  27490  lgsquad2lem2  27503  2lgslem1a1  27507  2lgslem1a2  27508  2lgslem1c  27511  2lgslem3a  27514  2lgslem3b  27515  2lgslem3c  27516  2lgslem3d  27517  2lgslem3  27522  2lgsoddprmlem1  27526  addsqrexnreu  27560  addsqnreup  27561  chebbnd1lem1  27587  chebbnd1lem3  27589  chebbnd1  27590  dchrisum0flblem2  27627  dchrisum0lem1  27634  mulog2sumlem2  27653  selberglem2  27664  chpdifbndlem1  27671  sltssnb  27916  mulscl  28281  ltmuls  28283  divs1  28351  precsexlem8  28361  0reno  28643  1reno  28644  slotsinbpsd  28664  slotslnbpsd  28665  ercgrg  28740  axlowdimlem4  29200  axlowdimlem5  29201  axlowdimlem6  29202  axlowdimlem7  29203  axlowdimlem8  29204  axlowdimlem10  29206  axlowdimlem11  29207  graop  29284  grastruct  29285  uhgrunop  29330  upgrop  29349  upgrunop  29374  umgrunop  29376  usgrop  29418  usgr2v1e2w  29507  usgrexmpldifpr  29513  usgrexmpledg  29517  uhgrsubgrself  29535  uhgrspan1lem1  29555  upgrres1lem1  29564  fusgrfis  29585  vtxd0nedgb  29743  p1evtxdeqlem  29767  p1evtxdeq  29768  p1evtxdp1  29769  umgr2v2e  29780  vdegp1bi  29792  wlkcomp  29885  upgr2pthnlp  29986  usgr2trlncl  30014  usgr2pthlem  30017  clwlkcomp  30033  uspgrn2crct  30062  wwlksonvtx  30109  wspthnonp  30113  2wlkond  30191  2pthond  30196  2pthon3v  30197  umgr2adedgwlkonALT  30201  umgr2wlk  30203  umgr2wlkon  30204  wpthswwlks2on  30218  elwspths2spth  30224  0ewlk  30370  0pth  30381  0pthonv  30385  1pthon2v  30409  3wlkdlem4  30418  3trlond  30429  3pthond  30431  3spthond  30433  trlsegvdeglem3  30478  eupthvdres  30491  eupth2lemb  30493  ex-natded5.2i  30662  ex-an  30678  ex-id  30690  ex-po  30691  ex-fl  30703  ex-mod  30705  ex-exp  30706  ex-lcm  30714  nvz0  30925  ipidsq  30967  ipdirilem  31086  siilem1  31108  minvecolem2  31132  minvecolem3  31133  minvecolem4  31137  hvsubcan  31331  hvsubcan2  31332  normlem7tALT  31376  helch  31500  hsn0elch  31505  hhshsslem2  31525  hhsssh  31526  shscli  31574  shintcli  31586  shintcl  31587  chintcli  31588  chintcl  31589  shincli  31619  shsval2i  31644  omlsi  31661  chincli  31717  chabs1  31773  fh1i  31878  fh2i  31879  cm2ji  31882  pjnormi  31978  nmopsetn0  32122  nmfnsetn0  32135  lnophm  32276  nmcexi  32283  nmbdfnlb  32307  imaelshi  32315  nlelshi  32317  nmopadjlem  32346  nmopcoadji  32358  hmopidmch  32410  hmopidmpj  32411  sto1i  32493  stlei  32497  stji1i  32499  csmdsymi  32591  chirred  32652  cdj3lem1  32691  rpdp2cl  33109  dp2lt10  33111  dp2lt  33112  dp2ltc  33114  dpfrac1  33119  dplti  33132  dpgti  33133  dpexpp1  33135  dpadd3  33139  dpmul  33140  dpmul4  33141  xrsclat  33239  nn0archi  33577  zringfrac  33756  cos9thpiminplylem4  34087  cos9thpiminplylem5  34088  cos9thpinconstr  34093  lmatfvlem  34117  xrge0iifmhm  34241  qqh0  34286  qqh1  34287  rerrext  34311  cnrrext  34312  prsiga  34433  oms0  34599  coinfliprv  34785  ballotlem1  34789  ballotth  34840  signsw0g  34855  hgt750lemd  34947  hgt750lem  34950  hgt750lem2  34951  hgt750leme  34957  tgoldbachgt  34962  subfacval2  35545  erdszelem2  35550  cvmliftlem4  35646  satom  35714  satfv1  35721  sat1el2xp  35737  fmlaomn0  35748  satfdmfmla  35758  satfv1fvfmla1  35781  ex-sategoelelomsuc  35784  ex-sategoelel12  35785  prv0  35788  prv1n  35789  elmrsubrn  35878  msubfval  35882  problem4  36026  quad3  36028  br6  36115  dfon2lem3  36141  fullfunfnv  36304  itgeq12i  36574  fneref  36718  filnetlem2  36747  filnetlem3  36748  onpsstopbas  36798  dfttc3gw  36891  dfttc4lem2  36897  dnizeq0  36921  dnibndlem12  36935  knoppcnlem5  36943  knoppcnlem8  36946  knoppcnlem11  36949  knoppndvlem14  36971  cnndvlem1  36983  bj-genr  37057  bj-genl  37058  bj-genan  37059  bj-2upln1upl  37516  bj-vtoclgfALT  37551  bj-brab2a1  37648  bj-opabssvv  37649  taupilem1  37820  qdiff  37826  topdifinf  37850  sin2h  38116  cos2h  38117  tan2h  38118  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem11  38137  poimirlem12  38138  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem22  38148  poimirlem23  38149  poimirlem24  38150  poimirlem25  38151  poimirlem26  38152  poimirlem29  38155  poimirlem31  38157  mblfinlem3  38165  mblfinlem4  38166  ismblfin  38167  itg2addnclem2  38178  asindmre  38209  heiborlem7  38323  riscer  38494  refrelcoss3  39059  symrelcoss3  39061  ishlatiN  39986  0psubN  40380  atpsubN  40384  gcdcomnni  42612  gcdnegnni  42613  neggcdnni  42614  60gcd7e1  42629  lcmeprodgcdi  42631  lcm2un  42638  lcm3un  42639  lcmineqlem4  42656  lcmineqlem6  42658  3lexlogpow5ineq1  42678  aks4d1p1p2  42694  mzpclall  43315  diophin  43360  diophun  43361  eldioph4b  43395  irrapx1  43412  2nn0ind  43529  aomclem4  43641  onexlimgt  43827  nnoeomeqom  43896  oaomoencom  43901  oenassex  43902  succlg  43912  dflim5  43913  omabs2  43916  tfsconcatfv2  43924  ifpid3g  44075  ifpid2g  44076  ifpbi1b  44086  eu0  44103  pwinfi  44147  rtrclex  44200  cnvrcl0  44208  dfrcl2  44257  relexp1idm  44297  relexp0idm  44298  clsk1independent  44629  lhe4.4ex1a  44898  expgrowth  44904  ax6e2nd  45126  uun0.1  45345  relopabVD  45468  ax6e2ndVD  45475  sb5ALTVD  45480  ax6e2ndALT  45497  permaxinf2lem  45580  rexanuz2nf  46065  dvmptconst  46488  dvmptidg  46490  dvmulcncf  46498  dvdivcncf  46500  dvnprodlem3  46521  itgsinexplem1  46527  volioof  46560  stoweidlem13  46586  stoweidlem14  46587  stoweidlem26  46599  stoweidlem34  46607  stoweidlem49  46622  stoweidlem59  46632  dirkertrigeqlem3  46673  dirkercncflem1  46676  dirkercncflem2  46677  fourierdlem57  46736  fourierdlem62  46741  fourierdlem103  46782  fourierdlem111  46790  fourierswlem  46803  fouriersw  46804  salexct2  46912  salexct3  46915  salgencntex  46916  salgensscntex  46917  gsumge0cl  46944  sge00  46949  sge0tsms  46953  0ome  47102  ovnlecvr  47131  ovn0lem  47138  hoidmvle  47173  ovnsubadd2lem  47218  smflimlem6  47349  mbfpsssmf  47356  smfmullem4  47367  smfpimbor1lem1  47371  nthrucw  47461  goldratmolem2  47479  cjnpoly  47482  sinnpoly  47484  astbstanbst  47502  aistbistaandb  47503  abnotataxb  47509  aifftbifffaibif  47514  confun4  47535  plcofph  47537  plvcofph  47539  plvcofphax  47540  plvofpos  47541  mdandyv0  47542  mdandyv1  47543  mdandyv2  47544  mdandyv3  47545  mdandyv4  47546  mdandyv5  47547  mdandyv6  47548  mdandyv7  47549  mdandyv8  47550  mdandyv9  47551  mdandyv10  47552  mdandyv11  47553  mdandyv12  47554  mdandyv13  47555  mdandyv14  47556  mdandyv15  47557  mdandyvr0  47558  mdandyvr1  47559  mdandyvr2  47560  mdandyvr3  47561  mdandyvr4  47562  mdandyvr5  47563  mdandyvr6  47564  mdandyvr7  47565  mdandyvrx0  47574  mdandyvrx1  47575  mdandyvrx2  47576  mdandyvrx3  47577  mdandyvrx4  47578  mdandyvrx5  47579  mdandyvrx6  47580  mdandyvrx7  47581  dandysum2p2e4  47591  or2expropbilem1  47625  dfnelbr2  47866  2ltceilhalf  47925  flmrecm1  47936  ich2exprop  48076  paireqne  48116  fmtno4prmfac  48180  31prm  48205  lighneallem4a  48216  41prothprmlem2  48226  ppivalnn4  48235  zofldiv2ALTV  48283  nfermltl8rev  48363  nfermltl2rev  48364  nfermltlrev  48365  gbegt5  48382  gbowgt5  48383  gboge9  48385  9gbo  48395  11gbo  48396  nnsum3primes4  48409  nnsum3primesgbe  48413  nnsum4primesodd  48417  nnsum4primesoddALTV  48418  nnsum4primeseven  48421  nnsum4primesevenALTV  48422  tgblthelfgott  48436  tgoldbach  48438  ushggricedg  48548  isubgrgrim  48550  stgrvtx  48575  stgriedg  48576  stgrusgra  48580  stgr1  48582  uspgrlim  48613  grlimprclnbgrvtx  48620  clnbgr3stgrgrlic  48641  usgrexmpl1lem  48642  usgrexmpl2lem  48647  usgrexmpl2nb0  48652  usgrexmpl2nb1  48653  usgrexmpl2nb2  48654  usgrexmpl2nb3  48655  usgrexmpl2nb4  48656  usgrexmpl2nb5  48657  gpgvtx  48664  gpgiedg  48665  gpgorder  48680  gpgvtxedg0  48684  gpgvtxedg1  48685  gpgedgiov  48686  gpg5nbgrvtx03starlem1  48689  gpg5nbgrvtx03starlem2  48690  gpg5nbgrvtx03starlem3  48691  gpg5nbgrvtx13starlem1  48692  gpg5nbgrvtx13starlem2  48693  gpg5nbgrvtx13starlem3  48694  gpg3kgrtriexlem3  48706  gpg3kgrtriexlem6  48709  gpgprismgr4cycllem2  48717  gpgprismgr4cyclex  48728  pgnioedg1  48729  pgnioedg2  48730  pgnioedg3  48731  pgnioedg4  48732  pgnioedg5  48733  pgnbgreunbgrlem2lem1  48735  pgnbgreunbgrlem2lem2  48736  pgnbgreunbgrlem2lem3  48737  pgnbgreunbgrlem3  48739  pgnbgreunbgrlem4  48740  pgnbgreunbgrlem5lem1  48741  pgnbgreunbgrlem5lem2  48742  pgnbgreunbgrlem5lem3  48743  pgnbgreunbgrlem6  48745  gpg5ngric  48749  gpg5edgnedg  48751  nn0mnd  48800  mgmplusgiopALT  48815  sgrp2sgrp  48849  2zrngaabl  48871  funcringcsetcALTV2lem8  48918  funcringcsetclem8ALTV  48941  zlmodzxzlmod  48986  zlmodzxzel  48987  zlmodzxzscm  48989  zlmodzxzadd  48990  snlindsntorlem  49102  ldepspr  49105  lmod1lem2  49120  lmod1lem3  49121  lmod1lem4  49122  lmod1lem5  49123  lmodn0  49127  zlmodzxznm  49129  zlmodzxzldeplem  49130  zlmodzxzldeplem1  49132  zlmodzxzldeplem3  49134  lvecpsslmod  49139  ldepsnlinc  49140  ldepslinc  49141  expnegico01  49150  zofldiv2  49163  flnn0div2ge  49165  elbigo2  49184  nnlog2ge0lt1  49198  digfval  49229  dignnld  49235  dignn0flhalf  49250  2arymaptfo  49286  itcovalt2lem1  49307  prelrrx2  49345  eenglngeehlnmlem2  49370  rrxsphere  49380  line2  49384  line2x  49386  line2y  49387  itsclc0yqsollem2  49395  inlinecirc02plem  49418  sepfsepc  49558  invfn  49660  alimp-surprise  50410  aacllem  50431