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  694  pm4.87  844  3pm3.2i  1341  unssi  4145  ssini  4194  opthhausdorff  5473  elvv  5707  elopaelxp  5722  relopabiv  5777  relopabi  5779  dfpo2  6262  funpr  6556  funcnvpr  6562  mpov  7480  caovcom  7565  snnex  7713  pwnex  7714  1st2val  7971  2nd2val  7972  elxp7  7978  opreuopreu  7988  poxp2  8095  poseq  8110  tfr1a  8335  oeoa  8535  oeoe  8537  erov  8763  endisj  9004  snopfsupp  9306  ssttrcl  9636  ttrclselem2  9647  r1funlim  9690  dfac2b  10053  cflecard  10175  canth4  10570  canthnumlem  10571  canthwelem  10573  canthp1lem2  10576  pwfseqlem4  10585  wunex3  10664  addsrpr  10998  mulsrpr  10999  recexsrlem  11026  mulcani  11788  div1  11843  recdiv  11859  divdiv1  11864  divdiv2  11865  div23i  11911  div11i  11912  divmuldivi  11913  divadddivi  11915  divdivdivi  11916  lemulge11  12016  negiso  12134  dfnn3  12171  2cnne0  12362  2rene0  12363  halfpm6th  12375  avglt1  12391  avglt2  12392  div4p1lem1div2  12408  3halfnz  12583  divlt1lt  12988  divle1le  12989  nnledivrp  13031  x2times  13226  xrsupsslem  13234  xrinfmsslem  13235  fvf1tp  13721  om2uzoi  13890  fzennn  13903  expge1  14034  sqoddm1div8  14178  faclbnd2  14226  faclbnd4lem1  14228  4bc2eq6  14264  hashfxnn0  14272  hashsnlei  14353  hashunlei  14360  hashsslei  14361  hash2prb  14407  repswccat  14721  funcnvs4  14850  f1oun2prg  14852  wrdlen2i  14877  s2rn  14898  s3rn  14899  s7rn  14900  relexpaddg  14988  cjreb  15058  sqrt2gt1lt2  15209  abs1m  15271  bpoly3  15993  ege2le3  16025  efi4p  16074  efival  16089  sin01bnd  16122  cos01bnd  16123  cos1bnd  16124  cos2bnd  16125  sin01gt0  16127  cos01gt0  16128  sin02gt0  16129  sincos2sgn  16131  sin4lt0  16132  egt2lt3  16143  rpnnen2lem3  16153  rpnnen2lem11  16161  nthruc  16189  nthruz  16190  3dvdsdec  16271  3dvds2dec  16272  mod2eq1n2dvds  16286  halfleoddlt  16301  divalglem5  16336  ndvdsi  16351  flodddiv4  16354  flodddiv4lt  16356  bitsp1o  16372  3lcm2e6woprm  16554  6lcm4e12  16555  pcrec  16798  prmrec  16862  prmgaplcmlem1  16991  prmgaplcm  17000  modsubi  17012  structfn  17095  strleun  17096  slotsdifipndx  17267  slotsdifplendx  17307  slotsdifdsndx  17326  slotsdifunifndx  17333  slotsdifplendx2  17348  slotsdifocndx  17349  isofn  17711  sscres  17759  funcestrcsetclem7  18081  funcestrcsetclem8  18082  fullestrcsetc  18086  nulchn  18554  chninf  18570  mgmnsgrpex  18868  pwmnd  18874  ga0  19239  symg2bas  19334  f1otrspeq  19388  psgnsn  19461  0frgp  19720  gsummptnn0fz  19927  srgbinomlem4  20176  isrnghm  20389  rnghmsscmap2  20574  rnghmsscmap  20575  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscmap2  20603  rhmsscmap  20604  funcringcsetc  20619  cnfldfun  21335  cnfldfunALT  21336  cnfldfunOLD  21348  cnfldfunALTOLD  21349  cnfld1  21360  cnfld1OLD  21361  cnsubdrglem  21385  expmhm  21403  expghm  21442  pzriprnglem4  21451  pzriprnglem9  21456  pzriprnglem14  21461  pzriprng1ALT  21463  psrbag0  22029  psrbagsn  22030  coe1fsupp  22167  coe1mul2  22223  evls1sca  22279  matmulr  22394  mat1dimelbas  22427  mat1f1o  22434  m2detleib  22587  smadiadetglem1  22627  pmatcollpw3fi1lem2  22743  cpmidpmatlem2  22827  cpmadumatpolylem1  22837  cayhamlem3  22843  cayhamlem4  22844  isbasis3g  22905  fctop  22960  cctop  22962  refref  23469  bl2in  24356  dscmet  24528  iihalf1  24893  iihalf2  24896  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  iscvsi  25097  zclmncvs  25116  ncvs1  25125  ehl2eudis  25390  minveclem2  25394  minveclem4  25400  ovolunlem1a  25465  volf  25498  i1f1lem  25658  mbfi1fseqlem5  25688  dveflem  25951  pilem2  26430  pilem3  26431  sinhalfpilem  26440  sincosq1lem  26474  tangtx  26482  sinq12gt0  26484  sincos4thpi  26490  sincos6thpi  26493  sincos3rdpi  26494  pigt3  26495  pige3ALT  26497  coseq1  26502  efeq1  26505  efif1olem4  26522  angneg  26781  ang180lem1  26787  1cubrlem  26819  quart1  26834  log2cnv  26922  log2tlbnd  26923  log2ublem1  26924  log2ub  26927  emcllem1  26974  emcllem6  26979  basellem1  27059  basellem2  27060  basellem3  27061  basellem8  27066  ppiublem1  27181  ppiublem2  27182  ppiub  27183  chtublem  27190  chtub  27191  bcmono  27256  bclbnd  27259  bpos1lem  27261  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem7  27269  bposlem8  27270  bposlem9  27271  lgsdir2lem1  27304  1lgs  27319  gausslemma2dlem0c  27337  gausslemma2dlem0d  27338  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem3  27347  gausslemma2dlem5  27350  gausslemma2dlem6  27351  lgsquad2lem2  27364  2lgslem1a1  27368  2lgslem1a2  27369  2lgslem1c  27372  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgslem3  27383  2lgsoddprmlem1  27387  addsqrexnreu  27421  addsqnreup  27422  chebbnd1lem1  27448  chebbnd1lem3  27450  chebbnd1  27451  dchrisum0flblem2  27488  dchrisum0lem1  27495  mulog2sumlem2  27514  selberglem2  27525  chpdifbndlem1  27532  sltssnb  27777  mulscl  28142  ltmuls  28144  divs1  28212  precsexlem8  28222  0reno  28504  1reno  28505  slotsinbpsd  28525  slotslnbpsd  28526  ercgrg  28601  axlowdimlem4  29030  axlowdimlem5  29031  axlowdimlem6  29032  axlowdimlem7  29033  axlowdimlem8  29034  axlowdimlem10  29036  axlowdimlem11  29037  graop  29114  grastruct  29115  uhgrunop  29160  upgrop  29179  upgrunop  29204  umgrunop  29206  usgrop  29248  usgr2v1e2w  29337  usgrexmpldifpr  29343  usgrexmpledg  29347  uhgrsubgrself  29365  uhgrspan1lem1  29385  upgrres1lem1  29394  fusgrfis  29415  vtxd0nedgb  29574  p1evtxdeqlem  29598  p1evtxdeq  29599  p1evtxdp1  29600  umgr2v2e  29611  vdegp1bi  29623  wlkcomp  29716  upgr2pthnlp  29817  usgr2trlncl  29845  usgr2pthlem  29848  clwlkcomp  29864  uspgrn2crct  29893  wwlksonvtx  29940  wspthnonp  29944  2wlkond  30022  2pthond  30027  2pthon3v  30028  umgr2adedgwlkonALT  30032  umgr2wlk  30034  umgr2wlkon  30035  wpthswwlks2on  30049  elwspths2spth  30055  0ewlk  30201  0pth  30212  0pthonv  30216  1pthon2v  30240  3wlkdlem4  30249  3trlond  30260  3pthond  30262  3spthond  30264  trlsegvdeglem3  30309  eupthvdres  30322  eupth2lemb  30324  ex-natded5.2i  30493  ex-an  30509  ex-id  30521  ex-po  30522  ex-fl  30534  ex-mod  30536  ex-exp  30537  ex-lcm  30545  nvz0  30755  ipidsq  30797  ipdirilem  30916  siilem1  30938  minvecolem2  30962  minvecolem3  30963  minvecolem4  30967  hvsubcan  31161  hvsubcan2  31162  normlem7tALT  31206  helch  31330  hsn0elch  31335  hhshsslem2  31355  hhsssh  31356  shscli  31404  shintcli  31416  shintcl  31417  chintcli  31418  chintcl  31419  shincli  31449  shsval2i  31474  omlsi  31491  chincli  31547  chabs1  31603  fh1i  31708  fh2i  31709  cm2ji  31712  pjnormi  31808  nmopsetn0  31952  nmfnsetn0  31965  lnophm  32106  nmcexi  32113  nmbdfnlb  32137  imaelshi  32145  nlelshi  32147  nmopadjlem  32176  nmopcoadji  32188  hmopidmch  32240  hmopidmpj  32241  sto1i  32323  stlei  32327  stji1i  32329  csmdsymi  32421  chirred  32482  cdj3lem1  32521  rpdp2cl  32973  dp2lt10  32975  dp2lt  32976  dp2ltc  32978  dpfrac1  32983  dplti  32996  dpgti  32997  dpexpp1  32999  dpadd3  33003  dpmul  33004  dpmul4  33005  xrsclat  33103  nn0archi  33439  zringfrac  33646  cos9thpiminplylem4  33962  cos9thpiminplylem5  33963  cos9thpinconstr  33968  lmatfvlem  33992  xrge0iifmhm  34116  qqh0  34161  qqh1  34162  rerrext  34186  cnrrext  34187  prsiga  34308  oms0  34474  coinfliprv  34660  ballotlem1  34664  ballotth  34715  signsw0g  34733  hgt750lemd  34825  hgt750lem  34828  hgt750lem2  34829  hgt750leme  34835  tgoldbachgt  34840  subfacval2  35400  erdszelem2  35405  cvmliftlem4  35501  satom  35569  satfv1  35576  sat1el2xp  35592  fmlaomn0  35603  satfdmfmla  35613  satfv1fvfmla1  35636  ex-sategoelelomsuc  35639  ex-sategoelel12  35640  prv0  35643  prv1n  35644  elmrsubrn  35733  msubfval  35737  problem4  35881  quad3  35883  br6  35970  dfon2lem3  35996  fullfunfnv  36159  itgeq12i  36419  fneref  36563  filnetlem2  36592  filnetlem3  36593  onpsstopbas  36643  exeltr  36684  dnizeq0  36694  dnibndlem12  36708  knoppcnlem5  36716  knoppcnlem8  36719  knoppcnlem11  36722  knoppndvlem14  36744  cnndvlem1  36756  bj-genr  36828  bj-genl  36829  bj-genan  36830  bj-2upln1upl  37266  bj-vtoclgfALT  37301  bj-brab2a1  37398  bj-opabssvv  37399  taupilem1  37570  topdifinf  37598  sin2h  37855  cos2h  37856  tan2h  37857  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem4  37869  poimirlem6  37871  poimirlem7  37872  poimirlem11  37876  poimirlem12  37877  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem22  37887  poimirlem23  37888  poimirlem24  37889  poimirlem25  37890  poimirlem26  37891  poimirlem29  37894  poimirlem31  37896  mblfinlem3  37904  mblfinlem4  37905  ismblfin  37906  itg2addnclem2  37917  asindmre  37948  heiborlem7  38062  riscer  38233  refrelcoss3  38798  symrelcoss3  38800  ishlatiN  39725  0psubN  40119  atpsubN  40123  gcdcomnni  42352  gcdnegnni  42353  neggcdnni  42354  60gcd7e1  42369  lcmeprodgcdi  42371  lcm2un  42378  lcm3un  42379  lcmineqlem4  42396  lcmineqlem6  42398  3lexlogpow5ineq1  42418  aks4d1p1p2  42434  mzpclall  43078  diophin  43123  diophun  43124  eldioph4b  43162  irrapx1  43179  2nn0ind  43296  aomclem4  43408  onexlimgt  43594  nnoeomeqom  43663  oaomoencom  43668  oenassex  43669  succlg  43679  dflim5  43680  omabs2  43683  tfsconcatfv2  43691  ifpid3g  43842  ifpid2g  43843  ifpbi1b  43853  eu0  43870  pwinfi  43914  rtrclex  43967  cnvrcl0  43975  dfrcl2  44024  relexp1idm  44064  relexp0idm  44065  clsk1independent  44396  lhe4.4ex1a  44679  expgrowth  44685  ax6e2nd  44908  uun0.1  45127  relopabVD  45250  ax6e2ndVD  45257  sb5ALTVD  45262  ax6e2ndALT  45279  permaxinf2lem  45362  rexanuz2nf  45844  dvmptconst  46267  dvmptidg  46269  dvmulcncf  46277  dvdivcncf  46279  dvnprodlem3  46300  itgsinexplem1  46306  volioof  46339  stoweidlem13  46365  stoweidlem14  46366  stoweidlem26  46378  stoweidlem34  46386  stoweidlem49  46401  stoweidlem59  46411  dirkertrigeqlem3  46452  dirkercncflem1  46455  dirkercncflem2  46456  fourierdlem57  46515  fourierdlem62  46520  fourierdlem103  46561  fourierdlem111  46569  fourierswlem  46582  fouriersw  46583  salexct2  46691  salexct3  46694  salgencntex  46695  salgensscntex  46696  gsumge0cl  46723  sge00  46728  sge0tsms  46732  0ome  46881  ovnlecvr  46910  ovn0lem  46917  hoidmvle  46952  ovnsubadd2lem  46997  smflimlem6  47128  mbfpsssmf  47135  smfmullem4  47146  smfpimbor1lem1  47150  nthrucw  47238  cjnpoly  47243  sinnpoly  47245  astbstanbst  47263  aistbistaandb  47264  abnotataxb  47270  aifftbifffaibif  47275  confun4  47296  plcofph  47298  plvcofph  47300  plvcofphax  47301  plvofpos  47302  mdandyv0  47303  mdandyv1  47304  mdandyv2  47305  mdandyv3  47306  mdandyv4  47307  mdandyv5  47308  mdandyv6  47309  mdandyv7  47310  mdandyv8  47311  mdandyv9  47312  mdandyv10  47313  mdandyv11  47314  mdandyv12  47315  mdandyv13  47316  mdandyv14  47317  mdandyv15  47318  mdandyvr0  47319  mdandyvr1  47320  mdandyvr2  47321  mdandyvr3  47322  mdandyvr4  47323  mdandyvr5  47324  mdandyvr6  47325  mdandyvr7  47326  mdandyvrx0  47335  mdandyvrx1  47336  mdandyvrx2  47337  mdandyvrx3  47338  mdandyvrx4  47339  mdandyvrx5  47340  mdandyvrx6  47341  mdandyvrx7  47342  dandysum2p2e4  47352  or2expropbilem1  47386  dfnelbr2  47627  2ltceilhalf  47682  ich2exprop  47825  paireqne  47865  fmtno4prmfac  47926  31prm  47951  lighneallem4a  47962  41prothprmlem2  47972  zofldiv2ALTV  48016  nfermltl8rev  48096  nfermltl2rev  48097  nfermltlrev  48098  gbegt5  48115  gbowgt5  48116  gboge9  48118  9gbo  48128  11gbo  48129  nnsum3primes4  48142  nnsum3primesgbe  48146  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  tgblthelfgott  48169  tgoldbach  48171  ushggricedg  48281  isubgrgrim  48283  stgrvtx  48308  stgriedg  48309  stgrusgra  48313  stgr1  48315  uspgrlim  48346  grlimprclnbgrvtx  48353  clnbgr3stgrgrlic  48374  usgrexmpl1lem  48375  usgrexmpl2lem  48380  usgrexmpl2nb0  48385  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2nb4  48389  usgrexmpl2nb5  48390  gpgvtx  48397  gpgiedg  48398  gpgorder  48413  gpgvtxedg0  48417  gpgvtxedg1  48418  gpgedgiov  48419  gpg5nbgrvtx03starlem1  48422  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx03starlem3  48424  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem2  48426  gpg5nbgrvtx13starlem3  48427  gpg3kgrtriexlem3  48439  gpg3kgrtriexlem6  48442  gpgprismgr4cycllem2  48450  gpgprismgr4cyclex  48461  pgnioedg1  48462  pgnioedg2  48463  pgnioedg3  48464  pgnioedg4  48465  pgnioedg5  48466  pgnbgreunbgrlem2lem1  48468  pgnbgreunbgrlem2lem2  48469  pgnbgreunbgrlem2lem3  48470  pgnbgreunbgrlem3  48472  pgnbgreunbgrlem4  48473  pgnbgreunbgrlem5lem1  48474  pgnbgreunbgrlem5lem2  48475  pgnbgreunbgrlem5lem3  48476  pgnbgreunbgrlem6  48478  gpg5ngric  48482  gpg5edgnedg  48484  nn0mnd  48533  mgmplusgiopALT  48548  sgrp2sgrp  48582  2zrngaabl  48604  funcringcsetcALTV2lem8  48651  funcringcsetclem8ALTV  48674  zlmodzxzlmod  48708  zlmodzxzel  48709  zlmodzxzscm  48711  zlmodzxzadd  48712  snlindsntorlem  48824  ldepspr  48827  lmod1lem2  48842  lmod1lem3  48843  lmod1lem4  48844  lmod1lem5  48845  lmodn0  48849  zlmodzxznm  48851  zlmodzxzldeplem  48852  zlmodzxzldeplem1  48854  zlmodzxzldeplem3  48856  lvecpsslmod  48861  ldepsnlinc  48862  ldepslinc  48863  expnegico01  48872  zofldiv2  48885  flnn0div2ge  48887  elbigo2  48906  nnlog2ge0lt1  48920  digfval  48951  dignnld  48957  dignn0flhalf  48972  2arymaptfo  49008  itcovalt2lem1  49029  prelrrx2  49067  eenglngeehlnmlem2  49092  rrxsphere  49102  line2  49106  line2x  49108  line2y  49109  itsclc0yqsollem2  49117  inlinecirc02plem  49140  sepfsepc  49281  invfn  49383  alimp-surprise  50133  aacllem  50154