Theorem pm3.2i 476

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

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mp4an  706  pm4.87  857  3pm3.2i  1358  unssi  4140  ssini  4188  opthhausdorff  5498  elvv  5734  elopaelxp  5749  relopabiv  5805  relopabi  5807  dfpo2  6298  funpr  6593  funcnvpr  6599  mpov  7529  caovcom  7615  snnex  7761  pwnex  7762  1st2val  8018  2nd2val  8019  elxp7  8025  opreuopreu  8035  poxp2  8145  poseq  8160  tfr1a  8387  oeoa  8589  oeoe  8591  erov  8818  endisj  9066  snopfsupp  9365  ssttrcl  9698  ttrclselem2  9709  r1funlim  9752  dfac2b  10137  cflecard  10258  canth4  10660  canthnumlem  10661  canthwelem  10663  canthp1lem2  10666  pwfseqlem4  10675  wunex3  10754  addsrpr  11088  mulsrpr  11089  recexsrlem  11116  mulcani  11881  div1  11932  recdiv  11949  divdiv1  11954  divdiv2  11955  div23i  12001  div11i  12002  divmuldivi  12003  divadddivi  12005  divdivdivi  12006  lemulge11  12105  negiso  12223  dfnn3  12275  2cnne0  12481  2rene0  12482  halfpm6th  12494  avglt1  12510  avglt2  12511  div4p1lem1div2  12527  3halfnz  12704  divlt1lt  13117  divle1le  13118  nnledivrp  13160  x2times  13355  xrsupsslem  13363  xrinfmsslem  13364  nnge2recico01  13564  fvf1tp  13854  om2uzoi  14023  fzennn  14036  expge1  14167  sqoddm1div8  14311  faclbnd2  14359  faclbnd4lem1  14361  4bc2eq6  14397  hashfxnn0  14405  hashsnlei  14487  hashunlei  14494  hashsslei  14495  hash2prb  14541  repswccat  14861  funcnvs4  14990  f1oun2prg  14992  wrdlen2i  15017  s2rn  15040  s3rn  15041  s7rn  15042  relexpaddg  15130  cjreb  15214  sqrt2gt1lt2  15365  abs1m  15427  bpoly3  16150  ege2le3  16182  efi4p  16231  efival  16246  sin01bnd  16279  cos01bnd  16280  cos1bnd  16281  cos2bnd  16282  sin01gt0  16284  cos01gt0  16285  sin02gt0  16286  sincos2sgn  16288  sin4lt0  16289  egt2lt3  16300  rpnnen2lem3  16310  rpnnen2lem11  16318  nthruc  16346  nthruz  16347  3dvdsdec  16428  3dvds2dec  16429  mod2eq1n2dvds  16443  halfleoddlt  16458  divalglem5  16493  ndvdsi  16508  flodddiv4  16511  flodddiv4lt  16513  bitsp1o  16529  3lcm2e6woprm  16711  6lcm4e12  16712  pcrec  16956  prmrec  17020  prmgaplcmlem1  17149  prmgaplcm  17158  modsubi  17170  structfn  17254  strleun  17255  slotsdifipndx  17426  slotsdifplendx  17466  slotsdifdsndx  17485  slotsdifunifndx  17492  slotsdifplendx2  17507  slotsdifocndx  17508  isofn  17870  sscres  17918  funcestrcsetclem7  18240  funcestrcsetclem8  18241  fullestrcsetc  18245  nulchn  18713  chninf  18729  mgmnsgrpex  19049  degenmgm  19056  degenmgm2nfun  19058  degenmgm2  19059  pwmnd  19062  ga0  19431  symg2bas  19526  f1otrspeq  19580  psgnsn  19653  0frgp  19912  gsummptnn0fz  20119  srgbinomlem4  20374  isrnghm  20588  rnghmsscmap2  20797  rnghmsscmap  20798  funcrngcsetc  20808  funcrngcsetcALT  20809  rhmsscmap2  20826  rhmsscmap  20827  funcringcsetc  20842  cnfldfun  21605  cnfldfunALT  21606  cnfld1  21616  cnsubdrglem  21637  expmhm  21655  expghm  21694  pzriprnglem4  21703  pzriprnglem9  21708  pzriprnglem14  21713  pzriprng1ALT  21715  psrbag0  22284  psrbagsn  22285  coe1fsupp  22445  coe1mul2  22501  evls1sca  22554  matmulr  22666  mat1dimelbas  22699  mat1f1o  22706  m2detleib  22859  smadiadetglem1  22899  pmatcollpw3fi1lem2  23018  cpmidpmatlem2  23102  cpmadumatpolylem1  23112  cayhamlem3  23118  cayhamlem4  23119  isbasis3g  23180  fctop  23235  cctop  23237  refref  23745  bl2in  24632  dscmet  24804  iihalf1  25165  iihalf2  25167  icopnfhmeo  25177  iccpnfhmeo  25179  xrhmeo  25180  iscvsi  25363  zclmncvs  25382  ncvs1  25391  ehl2eudis  25656  minveclem2  25660  minveclem4  25666  ovolunlem1a  25730  volf  25763  i1f1lem  25923  mbfi1fseqlem5  25953  dveflem  26213  pilem2  26695  pilem3  26696  sinhalfpilem  26708  sincosq1lem  26742  tangtx  26750  sinq12gt0  26752  sincos4thpi  26758  sincos6thpi  26761  sincos3rdpi  26762  pigt3  26763  pige3ALT  26765  coseq1  26770  efeq1  26773  efif1olem4  26790  angneg  27048  ang180lem1  27054  1cubrlem  27086  quart1  27101  log2cnv  27189  log2tlbnd  27190  log2ublem1  27191  log2ub  27194  emcllem1  27240  emcllem6  27245  basellem1  27325  basellem2  27326  basellem3  27327  basellem8  27332  ppiublem1  27446  ppiublem2  27447  ppiub  27448  chtublem  27455  chtub  27456  bcmono  27521  bclbnd  27524  bpos1lem  27526  bposlem1  27528  bposlem2  27529  bposlem3  27530  bposlem4  27531  bposlem5  27532  bposlem6  27533  bposlem7  27534  bposlem8  27535  bposlem9  27536  lgsdir2lem1  27569  1lgs  27584  gausslemma2dlem0c  27602  gausslemma2dlem0d  27603  gausslemma2dlem1a  27609  gausslemma2dlem2  27611  gausslemma2dlem3  27612  gausslemma2dlem5  27615  gausslemma2dlem6  27616  lgsquad2lem2  27629  2lgslem1a1  27633  2lgslem1a2  27634  2lgslem1c  27637  2lgslem3a  27640  2lgslem3b  27641  2lgslem3c  27642  2lgslem3d  27643  2lgslem3  27648  2lgsoddprmlem1  27652  addsqrexnreu  27686  addsqnreup  27687  chebbnd1lem1  27713  chebbnd1lem3  27715  chebbnd1  27716  dchrisum0flblem2  27753  dchrisum0lem1  27760  mulog2sumlem2  27779  selberglem2  27790  chpdifbndlem1  27797  sltssnb  28042  mulscl  28407  ltmuls  28409  divs1  28477  precsexlem8  28487  0reno  28769  1reno  28770  slotsinbpsd  28790  slotslnbpsd  28791  ercgrg  28867  axlowdimlem4  29410  axlowdimlem5  29411  axlowdimlem6  29412  axlowdimlem7  29413  axlowdimlem8  29414  axlowdimlem10  29416  axlowdimlem11  29417  graop  29494  grastruct  29495  uhgrunop  29540  upgrop  29559  upgrunop  29584  umgrunop  29586  usgrop  29631  usgr2v1e2w  29720  usgrexmpldifpr  29726  usgrexmpledg  29730  uhgrsubgrself  29748  uhgrspan1lem1  29768  upgrres1lem1  29777  fusgrfis  29798  vtxd0nedgb  29956  p1evtxdeqlem  29980  p1evtxdeq  29981  p1evtxdp1  29982  umgr2v2e  29993  vdegp1bi  30005  wlkcomp  30098  upgr2pthnlp  30205  usgr2trlncl  30233  usgr2pthlem  30236  clwlkcomp  30253  uspgrn2crct  30284  wwlksonvtx  30331  wspthnonp  30335  2wlkond  30413  2pthond  30418  2pthon3v  30419  umgr2adedgwlkonALT  30423  umgr2wlk  30425  umgr2wlkon  30426  wpthswwlks2on  30440  elwspths2spth  30446  0ewlk  30592  0pth  30603  0pthonv  30607  1pthon2v  30641  3wlkdlem4  30650  3trlond  30661  3pthond  30663  3spthond  30665  trlsegvdeglem3  30710  eupthvdres  30723  eupth2lemb  30725  ex-natded5.2i  30894  ex-an  30910  ex-id  30922  ex-po  30923  ex-fl  30935  ex-mod  30937  ex-exp  30938  ex-lcm  30946  nvz0  31157  ipidsq  31199  ipdirilem  31318  siilem1  31340  minvecolem2  31364  minvecolem3  31365  minvecolem4  31369  hvsubcan  31563  hvsubcan2  31564  normlem7tALT  31608  helch  31732  hsn0elch  31737  hhshsslem2  31757  hhsssh  31758  shscli  31806  shintcli  31818  shintcl  31819  chintcli  31820  chintcl  31821  shincli  31851  shsval2i  31876  omlsi  31893  chincli  31949  chabs1  32005  fh1i  32110  fh2i  32111  cm2ji  32114  pjnormi  32210  nmopsetn0  32354  nmfnsetn0  32367  lnophm  32508  nmcexi  32515  nmbdfnlb  32539  imaelshi  32547  nlelshi  32549  nmopadjlem  32578  nmopcoadji  32590  hmopidmch  32642  hmopidmpj  32643  sto1i  32725  stlei  32729  stji1i  32731  csmdsymi  32823  chirred  32884  cdj3lem1  32923  rpdp2cl  33335  dp2lt10  33337  dp2lt  33338  dp2ltc  33340  dpfrac1  33345  dplti  33358  dpgti  33359  dpexpp1  33361  dpadd3  33365  dpmul  33366  dpmul4  33367  xrsclat  33459  nn0archi  33795  zringfrac  33972  cos9thpiminplylem4  34303  cos9thpiminplylem5  34304  cos9thpinconstr  34309  lmatfvlem  34333  xrge0iifmhm  34457  qqh0  34502  qqh1  34503  rerrext  34527  cnrrext  34528  prsiga  34649  oms0  34816  coinfliprv  35002  ballotlem1  35006  ballotth  35057  signsw0g  35072  hgt750lemd  35164  hgt750lem  35167  hgt750lem2  35168  hgt750leme  35174  tgoldbachgt  35179  subfacval2  35774  erdszelem2  35779  cvmliftlem4  35875  satom  35943  satfv1  35950  sat1el2xp  35966  fmlaomn0  35977  satfdmfmla  35987  satfv1fvfmla1  36010  ex-sategoelelomsuc  36013  ex-sategoelel12  36014  prv0  36017  prv1n  36018  elmrsubrn  36107  msubfval  36111  problem4  36255  quad3  36257  br6  36344  dfon2lem3  36370  fullfunfnv  36533  itgeq12i  36834  fneref  36977  filnetlem2  37006  filnetlem3  37007  onpsstopbas  37057  dfttc3gw  37150  dfttc4lem2  37156  dnizeq0  37180  dnibndlem12  37194  knoppcnlem5  37202  knoppcnlem8  37205  knoppcnlem11  37208  knoppndvlem14  37230  cnndvlem1  37242  bj-genr  37316  bj-genl  37317  bj-genan  37318  bj-2upln1upl  37776  bj-vtoclgfALT  37811  bj-brab2a1  37909  bj-opabssvv  37910  taupilem1  38081  qdiff  38087  topdifinf  38111  sin2h  38372  cos2h  38373  tan2h  38374  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem11  38388  poimirlem12  38389  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem26  38403  poimirlem29  38406  poimirlem31  38408  mblfinlem3  38416  mblfinlem4  38417  ismblfin  38418  itg2addnclem2  38429  asindmre  38460  heiborlem7  38575  riscer  38746  refrelcoss3  39309  symrelcoss3  39311  ishlatiN  40236  0psubN  40630  atpsubN  40634  gcdcomnni  42862  gcdnegnni  42863  neggcdnni  42864  60gcd7e1  42879  lcmeprodgcdi  42881  lcm2un  42888  lcm3un  42889  lcmineqlem4  42906  lcmineqlem6  42908  3lexlogpow5ineq1  42928  aks4d1p1p2  42944  25or6to4  43080  mzpclall  43580  diophin  43625  diophun  43626  eldioph4b  43660  irrapx1  43677  2nn0ind  43794  aomclem4  43906  onexlimgt  44092  nnoeomeqom  44161  oaomoencom  44166  oenassex  44167  succlg  44177  dflim5  44178  omabs2  44181  tfsconcatfv2  44189  ifpid3g  44340  ifpid2g  44341  ifpbi1b  44351  eu0  44368  pwinfi  44412  rtrclex  44465  cnvrcl0  44473  dfrcl2  44522  relexp1idm  44562  relexp0idm  44563  clsk1independent  44894  lhe4.4ex1a  45161  expgrowth  45167  ax6e2nd  45389  uun0.1  45608  relopabVD  45731  ax6e2ndVD  45738  sb5ALTVD  45743  ax6e2ndALT  45760  permaxinf2lem  45843  rexanuz2nf  46328  dvmptconst  46751  dvmptidg  46753  dvmulcncf  46761  dvdivcncf  46763  dvnprodlem3  46784  itgsinexplem1  46790  volioof  46823  stoweidlem13  46849  stoweidlem14  46850  stoweidlem26  46862  stoweidlem34  46870  stoweidlem49  46885  stoweidlem59  46895  dirkertrigeqlem3  46936  dirkercncflem1  46939  dirkercncflem2  46940  fourierdlem57  46999  fourierdlem62  47004  fourierdlem103  47045  fourierdlem111  47053  fourierswlem  47066  fouriersw  47067  salexct2  47175  salexct3  47178  salgencntex  47179  salgensscntex  47180  gsumge0cl  47207  sge00  47212  sge0tsms  47216  0ome  47365  ovnlecvr  47394  ovn0lem  47401  hoidmvle  47436  ovnsubadd2lem  47481  smflimlem6  47612  mbfpsssmf  47619  smfmullem4  47630  smfpimbor1lem1  47634  sqrtnzqaa  47740  numtowerdt  47742  goldratmolem2  47759  sqrtnpoly  47769  astbstanbst  47805  aistbistaandb  47806  abnotataxb  47812  aifftbifffaibif  47817  confun4  47838  plcofph  47840  plvcofph  47842  plvcofphax  47843  plvofpos  47844  mdandyv0  47845  mdandyv1  47846  mdandyv2  47847  mdandyv3  47848  mdandyv4  47849  mdandyv5  47850  mdandyv6  47851  mdandyv7  47852  mdandyv8  47853  mdandyv9  47854  mdandyv10  47855  mdandyv11  47856  mdandyv12  47857  mdandyv13  47858  mdandyv14  47859  mdandyv15  47860  mdandyvr0  47861  mdandyvr1  47862  mdandyvr2  47863  mdandyvr3  47864  mdandyvr4  47865  mdandyvr5  47866  mdandyvr6  47867  mdandyvr7  47868  mdandyvrx0  47877  mdandyvrx1  47878  mdandyvrx2  47879  mdandyvrx3  47880  mdandyvrx4  47881  mdandyvrx5  47882  mdandyvrx6  47883  mdandyvrx7  47884  dandysum2p2e4  47894  or2expropbilem1  47928  dfnelbr2  48169  2ltceilhalf  48228  flmrecm1  48239  ich2exprop  48379  paireqne  48419  fmtno4prmfac  48483  31prm  48508  lighneallem4a  48519  41prothprmlem2  48529  ppivalnn4  48538  zofldiv2ALTV  48586  nfermltl8rev  48666  nfermltl2rev  48667  nfermltlrev  48668  gbegt5  48685  gbowgt5  48686  gboge9  48688  9gbo  48698  11gbo  48699  nnsum3primes4  48712  nnsum3primesgbe  48716  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  tgblthelfgott  48739  tgoldbach  48741  ushggricedg  48851  isubgrgrim  48853  stgrvtx  48878  stgriedg  48879  stgrusgra  48883  stgr1  48885  uspgrlim  48916  grlimprclnbgrvtx  48923  clnbgr3stgrgrlic  48944  usgrexmpl1lem  48945  usgrexmpl2lem  48950  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  gpgvtx  48967  gpgiedg  48968  gpgorder  48983  gpgvtxedg0  48987  gpgvtxedg1  48988  gpgedgiov  48989  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem2  48996  gpg5nbgrvtx13starlem3  48997  gpg3kgrtriexlem3  49009  gpg3kgrtriexlem6  49012  gpgprismgr4cycllem2  49020  gpgprismgr4cyclex  49031  pgnioedg1  49032  pgnioedg2  49033  pgnioedg3  49034  pgnioedg4  49035  pgnioedg5  49036  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem4  49043  pgnbgreunbgrlem5lem1  49044  pgnbgreunbgrlem5lem2  49045  pgnbgreunbgrlem5lem3  49046  pgnbgreunbgrlem6  49048  gpg5ngric  49052  gpg5edgnedg  49054  nn0mnd  49102  mgmplusgiopALT  49117  sgrp2sgrp  49151  2zrngaabl  49173  funcringcsetcALTV2lem8  49220  funcringcsetclem8ALTV  49243  zlmodzxzlmod  49292  zlmodzxzel  49293  zlmodzxzscm  49295  zlmodzxzadd  49296  snlindsntorlem  49408  ldepspr  49411  lmod1lem2  49426  lmod1lem3  49427  lmod1lem4  49428  lmod1lem5  49429  lmodn0  49433  zlmodzxznm  49435  zlmodzxzldeplem  49436  zlmodzxzldeplem1  49438  zlmodzxzldeplem3  49440  lvecpsslmod  49445  ldepsnlinc  49446  ldepslinc  49447  expnegico01  49456  zofldiv2  49469  flnn0div2ge  49471  elbigo2  49490  nnlog2ge0lt1  49504  digfval  49535  dignnld  49541  dignn0flhalf  49556  2arymaptfo  49592  itcovalt2lem1  49613  prelrrx2  49651  eenglngeehlnmlem2  49676  rrxsphere  49686  line2  49690  line2x  49692  line2y  49693  itsclc0yqsollem2  49701  inlinecirc02plem  49724  sepfsepc  49862  invfn  49964  alimp-surprise  50717  aacllem  50780