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  843  3pm3.2i  1340  unssi  4140  ssini  4189  opthhausdorff  5460  elvv  5694  elopaelxp  5709  relopabiv  5764  relopabi  5766  dfpo2  6248  funpr  6542  funcnvpr  6548  mpov  7464  caovcom  7549  snnex  7697  pwnex  7698  1st2val  7955  2nd2val  7956  elxp7  7962  opreuopreu  7972  poxp2  8079  poseq  8094  tfr1a  8319  oeoa  8518  oeoe  8520  erov  8744  endisj  8984  snopfsupp  9282  ssttrcl  9612  ttrclselem2  9623  r1funlim  9666  dfac2b  10029  cflecard  10151  canth4  10545  canthnumlem  10546  canthwelem  10548  canthp1lem2  10551  pwfseqlem4  10560  wunex3  10639  addsrpr  10973  mulsrpr  10974  recexsrlem  11001  mulcani  11763  div1  11818  recdiv  11834  divdiv1  11839  divdiv2  11840  div23i  11886  div11i  11887  divmuldivi  11888  divadddivi  11890  divdivdivi  11891  lemulge11  11991  negiso  12109  dfnn3  12146  2cnne0  12337  2rene0  12338  halfpm6th  12350  avglt1  12366  avglt2  12367  div4p1lem1div2  12383  3halfnz  12558  divlt1lt  12963  divle1le  12964  nnledivrp  13006  x2times  13200  xrsupsslem  13208  xrinfmsslem  13209  fvf1tp  13695  om2uzoi  13864  fzennn  13877  expge1  14008  sqoddm1div8  14152  faclbnd2  14200  faclbnd4lem1  14202  4bc2eq6  14238  hashfxnn0  14246  hashsnlei  14327  hashunlei  14334  hashsslei  14335  hash2prb  14381  repswccat  14695  funcnvs4  14824  f1oun2prg  14826  wrdlen2i  14851  s2rn  14872  s3rn  14873  s7rn  14874  relexpaddg  14962  cjreb  15032  sqrt2gt1lt2  15183  abs1m  15245  bpoly3  15967  ege2le3  15999  efi4p  16048  efival  16063  sin01bnd  16096  cos01bnd  16097  cos1bnd  16098  cos2bnd  16099  sin01gt0  16101  cos01gt0  16102  sin02gt0  16103  sincos2sgn  16105  sin4lt0  16106  egt2lt3  16117  rpnnen2lem3  16127  rpnnen2lem11  16135  nthruc  16163  nthruz  16164  3dvdsdec  16245  3dvds2dec  16246  mod2eq1n2dvds  16260  halfleoddlt  16275  divalglem5  16310  ndvdsi  16325  flodddiv4  16328  flodddiv4lt  16330  bitsp1o  16346  3lcm2e6woprm  16528  6lcm4e12  16529  pcrec  16772  prmrec  16836  prmgaplcmlem1  16965  prmgaplcm  16974  modsubi  16986  structfn  17069  strleun  17070  slotsdifipndx  17241  slotsdifplendx  17281  slotsdifdsndx  17300  slotsdifunifndx  17307  slotsdifplendx2  17322  slotsdifocndx  17323  isofn  17684  sscres  17732  funcestrcsetclem7  18054  funcestrcsetclem8  18055  fullestrcsetc  18059  nulchn  18527  chninf  18543  mgmnsgrpex  18841  pwmnd  18847  ga0  19212  symg2bas  19307  f1otrspeq  19361  psgnsn  19434  0frgp  19693  gsummptnn0fz  19900  srgbinomlem4  20149  isrnghm  20361  rnghmsscmap2  20546  rnghmsscmap  20547  funcrngcsetc  20557  funcrngcsetcALT  20558  rhmsscmap2  20575  rhmsscmap  20576  funcringcsetc  20591  cnfldfun  21307  cnfldfunALT  21308  cnfldfunOLD  21320  cnfldfunALTOLD  21321  cnfld1  21332  cnfld1OLD  21333  cnsubdrglem  21357  expmhm  21375  expghm  21414  pzriprnglem4  21423  pzriprnglem9  21428  pzriprnglem14  21433  pzriprng1ALT  21435  psrbag0  21998  psrbagsn  21999  coe1fsupp  22128  coe1mul2  22184  evls1sca  22239  matmulr  22354  mat1dimelbas  22387  mat1f1o  22394  m2detleib  22547  smadiadetglem1  22587  pmatcollpw3fi1lem2  22703  cpmidpmatlem2  22787  cpmadumatpolylem1  22797  cayhamlem3  22803  cayhamlem4  22804  isbasis3g  22865  fctop  22920  cctop  22922  refref  23429  bl2in  24316  dscmet  24488  iihalf1  24853  iihalf2  24856  icopnfhmeo  24869  iccpnfhmeo  24871  xrhmeo  24872  iscvsi  25057  zclmncvs  25076  ncvs1  25085  ehl2eudis  25350  minveclem2  25354  minveclem4  25360  ovolunlem1a  25425  volf  25458  i1f1lem  25618  mbfi1fseqlem5  25648  dveflem  25911  pilem2  26390  pilem3  26391  sinhalfpilem  26400  sincosq1lem  26434  tangtx  26442  sinq12gt0  26444  sincos4thpi  26450  sincos6thpi  26453  sincos3rdpi  26454  pigt3  26455  pige3ALT  26457  coseq1  26462  efeq1  26465  efif1olem4  26482  angneg  26741  ang180lem1  26747  1cubrlem  26779  quart1  26794  log2cnv  26882  log2tlbnd  26883  log2ublem1  26884  log2ub  26887  emcllem1  26934  emcllem6  26939  basellem1  27019  basellem2  27020  basellem3  27021  basellem8  27026  ppiublem1  27141  ppiublem2  27142  ppiub  27143  chtublem  27150  chtub  27151  bcmono  27216  bclbnd  27219  bpos1lem  27221  bposlem1  27223  bposlem2  27224  bposlem3  27225  bposlem4  27226  bposlem5  27227  bposlem6  27228  bposlem7  27229  bposlem8  27230  bposlem9  27231  lgsdir2lem1  27264  1lgs  27279  gausslemma2dlem0c  27297  gausslemma2dlem0d  27298  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  gausslemma2dlem3  27307  gausslemma2dlem5  27310  gausslemma2dlem6  27311  lgsquad2lem2  27324  2lgslem1a1  27328  2lgslem1a2  27329  2lgslem1c  27332  2lgslem3a  27335  2lgslem3b  27336  2lgslem3c  27337  2lgslem3d  27338  2lgslem3  27343  2lgsoddprmlem1  27347  addsqrexnreu  27381  addsqnreup  27382  chebbnd1lem1  27408  chebbnd1lem3  27410  chebbnd1  27411  dchrisum0flblem2  27448  dchrisum0lem1  27455  mulog2sumlem2  27474  selberglem2  27485  chpdifbndlem1  27492  ssltsnb  27733  mulscl  28074  sltmul  28076  divs1  28144  precsexlem8  28153  0reno  28400  slotsinbpsd  28420  slotslnbpsd  28421  ercgrg  28496  axlowdimlem4  28925  axlowdimlem5  28926  axlowdimlem6  28927  axlowdimlem7  28928  axlowdimlem8  28929  axlowdimlem10  28931  axlowdimlem11  28932  graop  29009  grastruct  29010  uhgrunop  29055  upgrop  29074  upgrunop  29099  umgrunop  29101  usgrop  29143  usgr2v1e2w  29232  usgrexmpldifpr  29238  usgrexmpledg  29242  uhgrsubgrself  29260  uhgrspan1lem1  29280  upgrres1lem1  29289  fusgrfis  29310  vtxd0nedgb  29469  p1evtxdeqlem  29493  p1evtxdeq  29494  p1evtxdp1  29495  umgr2v2e  29506  vdegp1bi  29518  wlkcomp  29611  upgr2pthnlp  29712  usgr2trlncl  29740  usgr2pthlem  29743  clwlkcomp  29759  uspgrn2crct  29788  wwlksonvtx  29835  wspthnonp  29839  2wlkond  29917  2pthond  29922  2pthon3v  29923  umgr2adedgwlkonALT  29927  umgr2wlk  29929  umgr2wlkon  29930  wpthswwlks2on  29944  elwspths2spth  29950  0ewlk  30096  0pth  30107  0pthonv  30111  1pthon2v  30135  3wlkdlem4  30144  3trlond  30155  3pthond  30157  3spthond  30159  trlsegvdeglem3  30204  eupthvdres  30217  eupth2lemb  30219  ex-natded5.2i  30388  ex-an  30404  ex-id  30416  ex-po  30417  ex-fl  30429  ex-mod  30431  ex-exp  30432  ex-lcm  30440  nvz0  30650  ipidsq  30692  ipdirilem  30811  siilem1  30833  minvecolem2  30857  minvecolem3  30858  minvecolem4  30862  hvsubcan  31056  hvsubcan2  31057  normlem7tALT  31101  helch  31225  hsn0elch  31230  hhshsslem2  31250  hhsssh  31251  shscli  31299  shintcli  31311  shintcl  31312  chintcli  31313  chintcl  31314  shincli  31344  shsval2i  31369  omlsi  31386  chincli  31442  chabs1  31498  fh1i  31603  fh2i  31604  cm2ji  31607  pjnormi  31703  nmopsetn0  31847  nmfnsetn0  31860  lnophm  32001  nmcexi  32008  nmbdfnlb  32032  imaelshi  32040  nlelshi  32042  nmopadjlem  32071  nmopcoadji  32083  hmopidmch  32135  hmopidmpj  32136  sto1i  32218  stlei  32222  stji1i  32224  csmdsymi  32316  chirred  32377  cdj3lem1  32416  rpdp2cl  32869  dp2lt10  32871  dp2lt  32872  dp2ltc  32874  dpfrac1  32879  dplti  32892  dpgti  32893  dpexpp1  32895  dpadd3  32899  dpmul  32900  dpmul4  32901  xrsclat  32999  nn0archi  33319  zringfrac  33526  cos9thpiminplylem4  33819  cos9thpiminplylem5  33820  cos9thpinconstr  33825  lmatfvlem  33849  xrge0iifmhm  33973  qqh0  34018  qqh1  34019  rerrext  34043  cnrrext  34044  prsiga  34165  oms0  34331  coinfliprv  34517  ballotlem1  34521  ballotth  34572  signsw0g  34590  hgt750lemd  34682  hgt750lem  34685  hgt750lem2  34686  hgt750leme  34692  tgoldbachgt  34697  subfacval2  35252  erdszelem2  35257  cvmliftlem4  35353  satom  35421  satfv1  35428  sat1el2xp  35444  fmlaomn0  35455  satfdmfmla  35465  satfv1fvfmla1  35488  ex-sategoelelomsuc  35491  ex-sategoelel12  35492  prv0  35495  prv1n  35496  elmrsubrn  35585  msubfval  35589  problem4  35733  quad3  35735  br6  35822  dfon2lem3  35848  fullfunfnv  36011  itgeq12i  36271  fneref  36415  filnetlem2  36444  filnetlem3  36445  onpsstopbas  36495  dnizeq0  36540  dnibndlem12  36554  knoppcnlem5  36562  knoppcnlem8  36565  knoppcnlem11  36568  knoppndvlem14  36590  cnndvlem1  36602  bj-genr  36671  bj-genl  36672  bj-genan  36673  bj-2upln1upl  37089  bj-vtoclgfALT  37124  bj-brab2a1  37214  bj-opabssvv  37215  taupilem1  37386  topdifinf  37414  sin2h  37670  cos2h  37671  tan2h  37672  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem4  37684  poimirlem6  37686  poimirlem7  37687  poimirlem11  37691  poimirlem12  37692  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem23  37703  poimirlem24  37704  poimirlem25  37705  poimirlem26  37706  poimirlem29  37709  poimirlem31  37711  mblfinlem3  37719  mblfinlem4  37720  ismblfin  37721  itg2addnclem2  37732  asindmre  37763  heiborlem7  37877  riscer  38048  refrelcoss3  38585  symrelcoss3  38587  ishlatiN  39474  0psubN  39868  atpsubN  39872  gcdcomnni  42101  gcdnegnni  42102  neggcdnni  42103  60gcd7e1  42118  lcmeprodgcdi  42120  lcm2un  42127  lcm3un  42128  lcmineqlem4  42145  lcmineqlem6  42147  3lexlogpow5ineq1  42167  aks4d1p1p2  42183  mzpclall  42844  diophin  42889  diophun  42890  eldioph4b  42928  irrapx1  42945  2nn0ind  43062  aomclem4  43174  onexlimgt  43360  nnoeomeqom  43429  oaomoencom  43434  oenassex  43435  succlg  43445  dflim5  43446  omabs2  43449  tfsconcatfv2  43457  ifpid3g  43609  ifpid2g  43610  ifpbi1b  43620  eu0  43637  pwinfi  43681  rtrclex  43734  cnvrcl0  43742  dfrcl2  43791  relexp1idm  43831  relexp0idm  43832  clsk1independent  44163  lhe4.4ex1a  44446  expgrowth  44452  ax6e2nd  44675  uun0.1  44894  relopabVD  45017  ax6e2ndVD  45024  sb5ALTVD  45029  ax6e2ndALT  45046  permaxinf2lem  45129  rexanuz2nf  45614  dvmptconst  46037  dvmptidg  46039  dvmulcncf  46047  dvdivcncf  46049  dvnprodlem3  46070  itgsinexplem1  46076  volioof  46109  stoweidlem13  46135  stoweidlem14  46136  stoweidlem26  46148  stoweidlem34  46156  stoweidlem49  46171  stoweidlem59  46181  dirkertrigeqlem3  46222  dirkercncflem1  46225  dirkercncflem2  46226  fourierdlem57  46285  fourierdlem62  46290  fourierdlem103  46331  fourierdlem111  46339  fourierswlem  46352  fouriersw  46353  salexct2  46461  salexct3  46464  salgencntex  46465  salgensscntex  46466  gsumge0cl  46493  sge00  46498  sge0tsms  46502  0ome  46651  ovnlecvr  46680  ovn0lem  46687  hoidmvle  46722  ovnsubadd2lem  46767  smflimlem6  46898  mbfpsssmf  46905  smfmullem4  46916  smfpimbor1lem1  46920  nthrucw  47008  cjnpoly  47013  sinnpoly  47015  astbstanbst  47033  aistbistaandb  47034  abnotataxb  47040  aifftbifffaibif  47045  confun4  47066  plcofph  47068  plvcofph  47070  plvcofphax  47071  plvofpos  47072  mdandyv0  47073  mdandyv1  47074  mdandyv2  47075  mdandyv3  47076  mdandyv4  47077  mdandyv5  47078  mdandyv6  47079  mdandyv7  47080  mdandyv8  47081  mdandyv9  47082  mdandyv10  47083  mdandyv11  47084  mdandyv12  47085  mdandyv13  47086  mdandyv14  47087  mdandyv15  47088  mdandyvr0  47089  mdandyvr1  47090  mdandyvr2  47091  mdandyvr3  47092  mdandyvr4  47093  mdandyvr5  47094  mdandyvr6  47095  mdandyvr7  47096  mdandyvrx0  47105  mdandyvrx1  47106  mdandyvrx2  47107  mdandyvrx3  47108  mdandyvrx4  47109  mdandyvrx5  47110  mdandyvrx6  47111  mdandyvrx7  47112  dandysum2p2e4  47122  or2expropbilem1  47156  dfnelbr2  47397  2ltceilhalf  47452  ich2exprop  47595  paireqne  47635  fmtno4prmfac  47696  31prm  47721  lighneallem4a  47732  41prothprmlem2  47742  zofldiv2ALTV  47786  nfermltl8rev  47866  nfermltl2rev  47867  nfermltlrev  47868  gbegt5  47885  gbowgt5  47886  gboge9  47888  9gbo  47898  11gbo  47899  nnsum3primes4  47912  nnsum3primesgbe  47916  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  tgblthelfgott  47939  tgoldbach  47941  ushggricedg  48051  isubgrgrim  48053  stgrvtx  48078  stgriedg  48079  stgrusgra  48083  stgr1  48085  uspgrlim  48116  grlimprclnbgrvtx  48123  clnbgr3stgrgrlic  48144  usgrexmpl1lem  48145  usgrexmpl2lem  48150  usgrexmpl2nb0  48155  usgrexmpl2nb1  48156  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  gpgvtx  48167  gpgiedg  48168  gpgorder  48183  gpgvtxedg0  48187  gpgvtxedg1  48188  gpgedgiov  48189  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpg3kgrtriexlem3  48209  gpg3kgrtriexlem6  48212  gpgprismgr4cycllem2  48220  gpgprismgr4cyclex  48231  pgnioedg1  48232  pgnioedg2  48233  pgnioedg3  48234  pgnioedg4  48235  pgnioedg5  48236  pgnbgreunbgrlem2lem1  48238  pgnbgreunbgrlem2lem2  48239  pgnbgreunbgrlem2lem3  48240  pgnbgreunbgrlem3  48242  pgnbgreunbgrlem4  48243  pgnbgreunbgrlem5lem1  48244  pgnbgreunbgrlem5lem2  48245  pgnbgreunbgrlem5lem3  48246  pgnbgreunbgrlem6  48248  gpg5ngric  48252  gpg5edgnedg  48254  nn0mnd  48303  mgmplusgiopALT  48318  sgrp2sgrp  48352  2zrngaabl  48374  funcringcsetcALTV2lem8  48421  funcringcsetclem8ALTV  48444  zlmodzxzlmod  48478  zlmodzxzel  48479  zlmodzxzscm  48481  zlmodzxzadd  48482  snlindsntorlem  48595  ldepspr  48598  lmod1lem2  48613  lmod1lem3  48614  lmod1lem4  48615  lmod1lem5  48616  lmodn0  48620  zlmodzxznm  48622  zlmodzxzldeplem  48623  zlmodzxzldeplem1  48625  zlmodzxzldeplem3  48627  lvecpsslmod  48632  ldepsnlinc  48633  ldepslinc  48634  expnegico01  48643  zofldiv2  48656  flnn0div2ge  48658  elbigo2  48677  nnlog2ge0lt1  48691  digfval  48722  dignnld  48728  dignn0flhalf  48743  2arymaptfo  48779  itcovalt2lem1  48800  prelrrx2  48838  eenglngeehlnmlem2  48863  rrxsphere  48873  line2  48877  line2x  48879  line2y  48880  itsclc0yqsollem2  48888  inlinecirc02plem  48911  sepfsepc  49052  invfn  49155  alimp-surprise  49905  aacllem  49926