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  4166  ssini  4215  opthhausdorff  5492  elvv  5729  elopaelxp  5744  relopabiv  5799  relopabi  5801  dfpo2  6285  funpr  6591  funcnvpr  6597  mpov  7517  caovcom  7602  snnex  7750  pwnex  7751  1st2val  8014  2nd2val  8015  elxp7  8021  opreuopreu  8031  mptmpoopabbrdOLDOLD  8080  poxp2  8140  poseq  8155  wfrlem13OLD  8333  wfr3OLD  8350  tfr1a  8406  oeoa  8607  oeoe  8609  erov  8826  endisj  9070  phplem2OLD  9227  snopfsupp  9401  ssttrcl  9727  ttrclselem2  9738  r1funlim  9778  dfac2b  10143  cflecard  10265  canth4  10659  canthnumlem  10660  canthwelem  10662  canthp1lem2  10665  pwfseqlem4  10674  wunex3  10753  addsrpr  11087  mulsrpr  11088  recexsrlem  11115  mulcani  11874  div1  11929  recdiv  11945  divdiv1  11950  divdiv2  11951  div23i  11997  div11i  11998  divmuldivi  11999  divadddivi  12001  divdivdivi  12002  lemulge11  12102  negiso  12220  dfnn3  12252  2cnne0  12448  2rene0  12449  halfpm6th  12461  avglt1  12477  avglt2  12478  div4p1lem1div2  12494  3halfnz  12670  divlt1lt  13076  divle1le  13077  nnledivrp  13119  x2times  13313  xrsupsslem  13321  xrinfmsslem  13322  fvf1tp  13804  om2uzoi  13971  fzennn  13984  expge1  14115  sqoddm1div8  14259  faclbnd2  14307  faclbnd4lem1  14309  4bc2eq6  14345  hashfxnn0  14353  hashsnlei  14434  hashunlei  14441  hashsslei  14442  hash2prb  14488  repswccat  14802  cshwsexaOLD  14841  funcnvs4  14932  f1oun2prg  14934  wrdlen2i  14959  s2rn  14980  s3rn  14981  s7rn  14982  relexpaddg  15070  cjreb  15140  sqrt2gt1lt2  15291  abs1m  15352  bpoly3  16072  ege2le3  16104  efi4p  16153  efival  16168  sin01bnd  16201  cos01bnd  16202  cos1bnd  16203  cos2bnd  16204  sin01gt0  16206  cos01gt0  16207  sin02gt0  16208  sincos2sgn  16210  sin4lt0  16211  egt2lt3  16222  rpnnen2lem3  16232  rpnnen2lem11  16240  nthruc  16268  nthruz  16269  3dvdsdec  16349  3dvds2dec  16350  mod2eq1n2dvds  16364  halfleoddlt  16379  divalglem5  16414  ndvdsi  16429  flodddiv4  16432  flodddiv4lt  16434  bitsp1o  16450  3lcm2e6woprm  16632  6lcm4e12  16633  pcrec  16876  prmrec  16940  prmgaplcmlem1  17069  prmgaplcm  17078  modsubi  17090  structfn  17173  strleun  17174  slotsdifipndx  17347  slotsdifplendx  17387  slotsdifdsndx  17406  slotsdifunifndx  17413  slotsdifplendx2  17428  slotsdifocndx  17429  isofn  17786  sscres  17834  funcestrcsetclem7  18156  funcestrcsetclem8  18157  fullestrcsetc  18161  mgmnsgrpex  18907  pwmnd  18913  ga0  19279  symg2bas  19372  f1otrspeq  19426  psgnsn  19499  0frgp  19758  gsummptnn0fz  19965  srgbinomlem4  20187  isrnghm  20399  rnghmsscmap2  20587  rnghmsscmap  20588  funcrngcsetc  20598  funcrngcsetcALT  20599  rhmsscmap2  20616  rhmsscmap  20617  funcringcsetc  20632  cnfldfun  21327  cnfldfunALT  21328  cnfldfunOLD  21340  cnfldfunALTOLD  21341  cnfld1  21354  cnfld1OLD  21355  cnsubdrglem  21384  expmhm  21402  expghm  21434  pzriprnglem4  21443  pzriprnglem9  21448  pzriprnglem14  21453  pzriprng1ALT  21455  psrbag0  22018  psrbagsn  22019  coe1fsupp  22148  coe1mul2  22204  evls1sca  22259  matmulr  22374  mat1dimelbas  22407  mat1f1o  22414  m2detleib  22567  smadiadetglem1  22607  pmatcollpw3fi1lem2  22723  cpmidpmatlem2  22807  cpmadumatpolylem1  22817  cayhamlem3  22823  cayhamlem4  22824  isbasis3g  22885  fctop  22940  cctop  22942  refref  23449  bl2in  24337  dscmet  24509  iihalf1  24874  iihalf2  24877  icopnfhmeo  24890  iccpnfhmeo  24892  xrhmeo  24893  iscvsi  25078  zclmncvs  25098  ncvs1  25107  ehl2eudis  25372  minveclem2  25376  minveclem4  25382  ovolunlem1a  25447  volf  25480  i1f1lem  25640  mbfi1fseqlem5  25670  dveflem  25933  pilem2  26412  pilem3  26413  sinhalfpilem  26422  sincosq1lem  26456  tangtx  26464  sinq12gt0  26466  sincos4thpi  26472  sincos6thpi  26475  sincos3rdpi  26476  pigt3  26477  pige3ALT  26479  coseq1  26484  efeq1  26487  efif1olem4  26504  angneg  26763  ang180lem1  26769  1cubrlem  26801  quart1  26816  log2cnv  26904  log2tlbnd  26905  log2ublem1  26906  log2ub  26909  emcllem1  26956  emcllem6  26961  basellem1  27041  basellem2  27042  basellem3  27043  basellem8  27048  ppiublem1  27163  ppiublem2  27164  ppiub  27165  chtublem  27172  chtub  27173  bcmono  27238  bclbnd  27241  bpos1lem  27243  bposlem1  27245  bposlem2  27246  bposlem3  27247  bposlem4  27248  bposlem5  27249  bposlem6  27250  bposlem7  27251  bposlem8  27252  bposlem9  27253  lgsdir2lem1  27286  1lgs  27301  gausslemma2dlem0c  27319  gausslemma2dlem0d  27320  gausslemma2dlem1a  27326  gausslemma2dlem2  27328  gausslemma2dlem3  27329  gausslemma2dlem5  27332  gausslemma2dlem6  27333  lgsquad2lem2  27346  2lgslem1a1  27350  2lgslem1a2  27351  2lgslem1c  27354  2lgslem3a  27357  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  2lgslem3  27365  2lgsoddprmlem1  27369  addsqrexnreu  27403  addsqnreup  27404  chebbnd1lem1  27430  chebbnd1lem3  27432  chebbnd1  27433  dchrisum0flblem2  27470  dchrisum0lem1  27477  mulog2sumlem2  27496  selberglem2  27507  chpdifbndlem1  27514  mulscl  28077  sltmul  28079  divs1  28146  precsexlem8  28155  nohalf  28324  0reno  28346  slotsinbpsd  28366  slotslnbpsd  28367  ercgrg  28442  axlowdimlem4  28870  axlowdimlem5  28871  axlowdimlem6  28872  axlowdimlem7  28873  axlowdimlem8  28874  axlowdimlem10  28876  axlowdimlem11  28877  graop  28954  grastruct  28955  uhgrunop  29000  upgrop  29019  upgrunop  29044  umgrunop  29046  usgrop  29088  usgr2v1e2w  29177  usgrexmpldifpr  29183  usgrexmpledg  29187  uhgrsubgrself  29205  uhgrspan1lem1  29225  upgrres1lem1  29234  fusgrfis  29255  vtxd0nedgb  29414  p1evtxdeqlem  29438  p1evtxdeq  29439  p1evtxdp1  29440  umgr2v2e  29451  vdegp1bi  29463  wlkcomp  29557  upgr2pthnlp  29660  usgr2trlncl  29688  usgr2pthlem  29691  clwlkcomp  29707  uspgrn2crct  29736  wwlksonvtx  29783  wspthnonp  29787  2wlkond  29865  2pthond  29870  2pthon3v  29871  umgr2adedgwlkonALT  29875  umgr2wlk  29877  umgr2wlkon  29878  wpthswwlks2on  29889  elwspths2spth  29895  0ewlk  30041  0pth  30052  0pthonv  30056  1pthon2v  30080  3wlkdlem4  30089  3trlond  30100  3pthond  30102  3spthond  30104  trlsegvdeglem3  30149  eupthvdres  30162  eupth2lemb  30164  ex-natded5.2i  30333  ex-an  30349  ex-id  30361  ex-po  30362  ex-fl  30374  ex-mod  30376  ex-exp  30377  ex-lcm  30385  nvz0  30595  ipidsq  30637  ipdirilem  30756  siilem1  30778  minvecolem2  30802  minvecolem3  30803  minvecolem4  30807  hvsubcan  31001  hvsubcan2  31002  normlem7tALT  31046  helch  31170  hsn0elch  31175  hhshsslem2  31195  hhsssh  31196  shscli  31244  shintcli  31256  shintcl  31257  chintcli  31258  chintcl  31259  shincli  31289  shsval2i  31314  omlsi  31331  chincli  31387  chabs1  31443  fh1i  31548  fh2i  31549  cm2ji  31552  pjnormi  31648  nmopsetn0  31792  nmfnsetn0  31805  lnophm  31946  nmcexi  31953  nmbdfnlb  31977  imaelshi  31985  nlelshi  31987  nmopadjlem  32016  nmopcoadji  32028  hmopidmch  32080  hmopidmpj  32081  sto1i  32163  stlei  32167  stji1i  32169  csmdsymi  32261  chirred  32322  cdj3lem1  32361  rpdp2cl  32802  dp2lt10  32804  dp2lt  32805  dp2ltc  32807  dpfrac1  32812  dplti  32825  dpgti  32826  dpexpp1  32828  dpadd3  32832  dpmul  32833  dpmul4  32834  xrsclat  32949  nn0archi  33308  zringfrac  33515  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  lmatfvlem  33792  xrge0iifmhm  33916  qqh0  33961  qqh1  33962  rerrext  33986  cnrrext  33987  prsiga  34108  oms0  34275  coinfliprv  34461  ballotlem1  34465  ballotth  34516  signsw0g  34534  hgt750lemd  34626  hgt750lem  34629  hgt750lem2  34630  hgt750leme  34636  tgoldbachgt  34641  subfacval2  35155  erdszelem2  35160  cvmliftlem4  35256  satom  35324  satfv1  35331  sat1el2xp  35347  fmlaomn0  35358  satfdmfmla  35368  satfv1fvfmla1  35391  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  prv0  35398  prv1n  35399  elmrsubrn  35488  msubfval  35492  problem4  35636  quad3  35638  br6  35720  dfon2lem3  35749  fullfunfnv  35910  itgeq12i  36170  fneref  36314  filnetlem2  36343  filnetlem3  36344  onpsstopbas  36394  dnizeq0  36439  dnibndlem12  36453  knoppcnlem5  36461  knoppcnlem8  36464  knoppcnlem11  36467  knoppndvlem14  36489  cnndvlem1  36501  bj-genr  36570  bj-genl  36571  bj-genan  36572  bj-2upln1upl  36988  bj-vtoclgfALT  37023  bj-brab2a1  37113  bj-opabssvv  37114  taupilem1  37285  topdifinf  37313  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem4  37594  poimirlem6  37596  poimirlem7  37597  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem29  37619  poimirlem31  37621  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  itg2addnclem2  37642  asindmre  37673  heiborlem7  37787  riscer  37958  refrelcoss3  38427  symrelcoss3  38429  ishlatiN  39319  0psubN  39714  atpsubN  39718  gcdcomnni  41947  gcdnegnni  41948  neggcdnni  41949  60gcd7e1  41964  lcmeprodgcdi  41966  lcm2un  41973  lcm3un  41974  lcmineqlem4  41991  lcmineqlem6  41993  3lexlogpow5ineq1  42013  aks4d1p1p2  42029  mzpclall  42697  diophin  42742  diophun  42743  eldioph4b  42781  irrapx1  42798  2nn0ind  42916  aomclem4  43028  onexlimgt  43214  nnoeomeqom  43283  oaomoencom  43288  oenassex  43289  succlg  43299  dflim5  43300  omabs2  43303  tfsconcatfv2  43311  ifpid3g  43463  ifpid2g  43464  ifpbi1b  43474  eu0  43491  pwinfi  43535  rtrclex  43588  cnvrcl0  43596  dfrcl2  43645  relexp1idm  43685  relexp0idm  43686  clsk1independent  44017  lhe4.4ex1a  44301  expgrowth  44307  ax6e2nd  44531  uun0.1  44750  relopabVD  44873  ax6e2ndVD  44880  sb5ALTVD  44885  ax6e2ndALT  44902  permaxinf2lem  44985  rexanuz2nf  45467  dvmptconst  45892  dvmptidg  45894  dvmulcncf  45902  dvdivcncf  45904  dvnprodlem3  45925  itgsinexplem1  45931  volioof  45964  stoweidlem13  45990  stoweidlem14  45991  stoweidlem26  46003  stoweidlem34  46011  stoweidlem49  46026  stoweidlem59  46036  dirkertrigeqlem3  46077  dirkercncflem1  46080  dirkercncflem2  46081  fourierdlem57  46140  fourierdlem62  46145  fourierdlem103  46186  fourierdlem111  46194  fourierswlem  46207  fouriersw  46208  salexct2  46316  salexct3  46319  salgencntex  46320  salgensscntex  46321  gsumge0cl  46348  sge00  46353  sge0tsms  46357  0ome  46506  ovnlecvr  46535  ovn0lem  46542  hoidmvle  46577  ovnsubadd2lem  46622  smflimlem6  46753  mbfpsssmf  46760  smfmullem4  46771  smfpimbor1lem1  46775  astbstanbst  46886  aistbistaandb  46887  abnotataxb  46893  aifftbifffaibif  46898  confun4  46919  plcofph  46921  plvcofph  46923  plvcofphax  46924  plvofpos  46925  mdandyv0  46926  mdandyv1  46927  mdandyv2  46928  mdandyv3  46929  mdandyv4  46930  mdandyv5  46931  mdandyv6  46932  mdandyv7  46933  mdandyv8  46934  mdandyv9  46935  mdandyv10  46936  mdandyv11  46937  mdandyv12  46938  mdandyv13  46939  mdandyv14  46940  mdandyv15  46941  mdandyvr0  46942  mdandyvr1  46943  mdandyvr2  46944  mdandyvr3  46945  mdandyvr4  46946  mdandyvr5  46947  mdandyvr6  46948  mdandyvr7  46949  mdandyvrx0  46958  mdandyvrx1  46959  mdandyvrx2  46960  mdandyvrx3  46961  mdandyvrx4  46962  mdandyvrx5  46963  mdandyvrx6  46964  mdandyvrx7  46965  dandysum2p2e4  46975  or2expropbilem1  47009  dfnelbr2  47250  2ltceilhalf  47305  ich2exprop  47433  paireqne  47473  fmtno4prmfac  47534  31prm  47559  lighneallem4a  47570  41prothprmlem2  47580  zofldiv2ALTV  47624  nfermltl8rev  47704  nfermltl2rev  47705  nfermltlrev  47706  gbegt5  47723  gbowgt5  47724  gboge9  47726  9gbo  47736  11gbo  47737  nnsum3primes4  47750  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  tgblthelfgott  47777  tgoldbach  47779  ushggricedg  47888  isubgrgrim  47890  stgrvtx  47914  stgriedg  47915  stgrusgra  47919  stgr1  47921  uspgrlim  47952  clnbgr3stgrgrlic  47972  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  gpgvtx  47995  gpgiedg  47996  gpgorder  48011  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg3kgrtriexlem3  48035  gpg3kgrtriexlem6  48038  gpgprismgr4cycllem2  48043  gpgprismgr4cyclex  48054  nn0mnd  48102  mgmplusgiopALT  48117  sgrp2sgrp  48151  2zrngaabl  48173  funcringcsetcALTV2lem8  48220  funcringcsetclem8ALTV  48243  zlmodzxzlmod  48277  zlmodzxzel  48278  zlmodzxzscm  48280  zlmodzxzadd  48281  snlindsntorlem  48394  ldepspr  48397  lmod1lem2  48412  lmod1lem3  48413  lmod1lem4  48414  lmod1lem5  48415  lmodn0  48419  zlmodzxznm  48421  zlmodzxzldeplem  48422  zlmodzxzldeplem1  48424  zlmodzxzldeplem3  48426  lvecpsslmod  48431  ldepsnlinc  48432  ldepslinc  48433  expnegico01  48442  zofldiv2  48459  flnn0div2ge  48461  elbigo2  48480  nnlog2ge0lt1  48494  digfval  48525  dignnld  48531  dignn0flhalf  48546  2arymaptfo  48582  itcovalt2lem1  48603  prelrrx2  48641  eenglngeehlnmlem2  48666  rrxsphere  48676  line2  48680  line2x  48682  line2y  48683  itsclc0yqsollem2  48691  inlinecirc02plem  48714  sepfsepc  48850  invfn  48948  alimp-surprise  49592  aacllem  49613