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  4157  ssini  4206  opthhausdorff  5480  elvv  5716  elopaelxp  5731  relopabiv  5786  relopabi  5788  dfpo2  6272  funpr  6575  funcnvpr  6581  mpov  7504  caovcom  7589  snnex  7737  pwnex  7738  1st2val  7999  2nd2val  8000  elxp7  8006  opreuopreu  8016  mptmpoopabbrdOLDOLD  8065  poxp2  8125  poseq  8140  tfr1a  8365  oeoa  8564  oeoe  8566  erov  8790  endisj  9032  snopfsupp  9349  ssttrcl  9675  ttrclselem2  9686  r1funlim  9726  dfac2b  10091  cflecard  10213  canth4  10607  canthnumlem  10608  canthwelem  10610  canthp1lem2  10613  pwfseqlem4  10622  wunex3  10701  addsrpr  11035  mulsrpr  11036  recexsrlem  11063  mulcani  11824  div1  11879  recdiv  11895  divdiv1  11900  divdiv2  11901  div23i  11947  div11i  11948  divmuldivi  11949  divadddivi  11951  divdivdivi  11952  lemulge11  12052  negiso  12170  dfnn3  12207  2cnne0  12398  2rene0  12399  halfpm6th  12411  avglt1  12427  avglt2  12428  div4p1lem1div2  12444  3halfnz  12620  divlt1lt  13029  divle1le  13030  nnledivrp  13072  x2times  13266  xrsupsslem  13274  xrinfmsslem  13275  fvf1tp  13758  om2uzoi  13927  fzennn  13940  expge1  14071  sqoddm1div8  14215  faclbnd2  14263  faclbnd4lem1  14265  4bc2eq6  14301  hashfxnn0  14309  hashsnlei  14390  hashunlei  14397  hashsslei  14398  hash2prb  14444  repswccat  14758  cshwsexaOLD  14797  funcnvs4  14888  f1oun2prg  14890  wrdlen2i  14915  s2rn  14936  s3rn  14937  s7rn  14938  relexpaddg  15026  cjreb  15096  sqrt2gt1lt2  15247  abs1m  15309  bpoly3  16031  ege2le3  16063  efi4p  16112  efival  16127  sin01bnd  16160  cos01bnd  16161  cos1bnd  16162  cos2bnd  16163  sin01gt0  16165  cos01gt0  16166  sin02gt0  16167  sincos2sgn  16169  sin4lt0  16170  egt2lt3  16181  rpnnen2lem3  16191  rpnnen2lem11  16199  nthruc  16227  nthruz  16228  3dvdsdec  16309  3dvds2dec  16310  mod2eq1n2dvds  16324  halfleoddlt  16339  divalglem5  16374  ndvdsi  16389  flodddiv4  16392  flodddiv4lt  16394  bitsp1o  16410  3lcm2e6woprm  16592  6lcm4e12  16593  pcrec  16836  prmrec  16900  prmgaplcmlem1  17029  prmgaplcm  17038  modsubi  17050  structfn  17133  strleun  17134  slotsdifipndx  17305  slotsdifplendx  17345  slotsdifdsndx  17364  slotsdifunifndx  17371  slotsdifplendx2  17386  slotsdifocndx  17387  isofn  17744  sscres  17792  funcestrcsetclem7  18114  funcestrcsetclem8  18115  fullestrcsetc  18119  mgmnsgrpex  18865  pwmnd  18871  ga0  19237  symg2bas  19330  f1otrspeq  19384  psgnsn  19457  0frgp  19716  gsummptnn0fz  19923  srgbinomlem4  20145  isrnghm  20357  rnghmsscmap2  20545  rnghmsscmap  20546  funcrngcsetc  20556  funcrngcsetcALT  20557  rhmsscmap2  20574  rhmsscmap  20575  funcringcsetc  20590  cnfldfun  21285  cnfldfunALT  21286  cnfldfunOLD  21298  cnfldfunALTOLD  21299  cnfld1  21312  cnfld1OLD  21313  cnsubdrglem  21342  expmhm  21360  expghm  21392  pzriprnglem4  21401  pzriprnglem9  21406  pzriprnglem14  21411  pzriprng1ALT  21413  psrbag0  21976  psrbagsn  21977  coe1fsupp  22106  coe1mul2  22162  evls1sca  22217  matmulr  22332  mat1dimelbas  22365  mat1f1o  22372  m2detleib  22525  smadiadetglem1  22565  pmatcollpw3fi1lem2  22681  cpmidpmatlem2  22765  cpmadumatpolylem1  22775  cayhamlem3  22781  cayhamlem4  22782  isbasis3g  22843  fctop  22898  cctop  22900  refref  23407  bl2in  24295  dscmet  24467  iihalf1  24832  iihalf2  24835  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  iscvsi  25036  zclmncvs  25055  ncvs1  25064  ehl2eudis  25329  minveclem2  25333  minveclem4  25339  ovolunlem1a  25404  volf  25437  i1f1lem  25597  mbfi1fseqlem5  25627  dveflem  25890  pilem2  26369  pilem3  26370  sinhalfpilem  26379  sincosq1lem  26413  tangtx  26421  sinq12gt0  26423  sincos4thpi  26429  sincos6thpi  26432  sincos3rdpi  26433  pigt3  26434  pige3ALT  26436  coseq1  26441  efeq1  26444  efif1olem4  26461  angneg  26720  ang180lem1  26726  1cubrlem  26758  quart1  26773  log2cnv  26861  log2tlbnd  26862  log2ublem1  26863  log2ub  26866  emcllem1  26913  emcllem6  26918  basellem1  26998  basellem2  26999  basellem3  27000  basellem8  27005  ppiublem1  27120  ppiublem2  27121  ppiub  27122  chtublem  27129  chtub  27130  bcmono  27195  bclbnd  27198  bpos1lem  27200  bposlem1  27202  bposlem2  27203  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem7  27208  bposlem8  27209  bposlem9  27210  lgsdir2lem1  27243  1lgs  27258  gausslemma2dlem0c  27276  gausslemma2dlem0d  27277  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  gausslemma2dlem3  27286  gausslemma2dlem5  27289  gausslemma2dlem6  27290  lgsquad2lem2  27303  2lgslem1a1  27307  2lgslem1a2  27308  2lgslem1c  27311  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgslem3  27322  2lgsoddprmlem1  27326  addsqrexnreu  27360  addsqnreup  27361  chebbnd1lem1  27387  chebbnd1lem3  27389  chebbnd1  27390  dchrisum0flblem2  27427  dchrisum0lem1  27434  mulog2sumlem2  27453  selberglem2  27464  chpdifbndlem1  27471  mulscl  28044  sltmul  28046  divs1  28114  precsexlem8  28123  0reno  28355  slotsinbpsd  28375  slotslnbpsd  28376  ercgrg  28451  axlowdimlem4  28879  axlowdimlem5  28880  axlowdimlem6  28881  axlowdimlem7  28882  axlowdimlem8  28883  axlowdimlem10  28885  axlowdimlem11  28886  graop  28963  grastruct  28964  uhgrunop  29009  upgrop  29028  upgrunop  29053  umgrunop  29055  usgrop  29097  usgr2v1e2w  29186  usgrexmpldifpr  29192  usgrexmpledg  29196  uhgrsubgrself  29214  uhgrspan1lem1  29234  upgrres1lem1  29243  fusgrfis  29264  vtxd0nedgb  29423  p1evtxdeqlem  29447  p1evtxdeq  29448  p1evtxdp1  29449  umgr2v2e  29460  vdegp1bi  29472  wlkcomp  29566  upgr2pthnlp  29669  usgr2trlncl  29697  usgr2pthlem  29700  clwlkcomp  29716  uspgrn2crct  29745  wwlksonvtx  29792  wspthnonp  29796  2wlkond  29874  2pthond  29879  2pthon3v  29880  umgr2adedgwlkonALT  29884  umgr2wlk  29886  umgr2wlkon  29887  wpthswwlks2on  29898  elwspths2spth  29904  0ewlk  30050  0pth  30061  0pthonv  30065  1pthon2v  30089  3wlkdlem4  30098  3trlond  30109  3pthond  30111  3spthond  30113  trlsegvdeglem3  30158  eupthvdres  30171  eupth2lemb  30173  ex-natded5.2i  30342  ex-an  30358  ex-id  30370  ex-po  30371  ex-fl  30383  ex-mod  30385  ex-exp  30386  ex-lcm  30394  nvz0  30604  ipidsq  30646  ipdirilem  30765  siilem1  30787  minvecolem2  30811  minvecolem3  30812  minvecolem4  30816  hvsubcan  31010  hvsubcan2  31011  normlem7tALT  31055  helch  31179  hsn0elch  31184  hhshsslem2  31204  hhsssh  31205  shscli  31253  shintcli  31265  shintcl  31266  chintcli  31267  chintcl  31268  shincli  31298  shsval2i  31323  omlsi  31340  chincli  31396  chabs1  31452  fh1i  31557  fh2i  31558  cm2ji  31561  pjnormi  31657  nmopsetn0  31801  nmfnsetn0  31814  lnophm  31955  nmcexi  31962  nmbdfnlb  31986  imaelshi  31994  nlelshi  31996  nmopadjlem  32025  nmopcoadji  32037  hmopidmch  32089  hmopidmpj  32090  sto1i  32172  stlei  32176  stji1i  32178  csmdsymi  32270  chirred  32331  cdj3lem1  32370  rpdp2cl  32809  dp2lt10  32811  dp2lt  32812  dp2ltc  32814  dpfrac1  32819  dplti  32832  dpgti  32833  dpexpp1  32835  dpadd3  32839  dpmul  32840  dpmul4  32841  xrsclat  32956  nn0archi  33325  zringfrac  33532  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  cos9thpinconstr  33788  lmatfvlem  33812  xrge0iifmhm  33936  qqh0  33981  qqh1  33982  rerrext  34006  cnrrext  34007  prsiga  34128  oms0  34295  coinfliprv  34481  ballotlem1  34485  ballotth  34536  signsw0g  34554  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  tgoldbachgt  34661  subfacval2  35181  erdszelem2  35186  cvmliftlem4  35282  satom  35350  satfv1  35357  sat1el2xp  35373  fmlaomn0  35384  satfdmfmla  35394  satfv1fvfmla1  35417  ex-sategoelelomsuc  35420  ex-sategoelel12  35421  prv0  35424  prv1n  35425  elmrsubrn  35514  msubfval  35518  problem4  35662  quad3  35664  br6  35751  dfon2lem3  35780  fullfunfnv  35941  itgeq12i  36201  fneref  36345  filnetlem2  36374  filnetlem3  36375  onpsstopbas  36425  dnizeq0  36470  dnibndlem12  36484  knoppcnlem5  36492  knoppcnlem8  36495  knoppcnlem11  36498  knoppndvlem14  36520  cnndvlem1  36532  bj-genr  36601  bj-genl  36602  bj-genan  36603  bj-2upln1upl  37019  bj-vtoclgfALT  37054  bj-brab2a1  37144  bj-opabssvv  37145  taupilem1  37316  topdifinf  37344  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem29  37650  poimirlem31  37652  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnclem2  37673  asindmre  37704  heiborlem7  37818  riscer  37989  refrelcoss3  38461  symrelcoss3  38463  ishlatiN  39355  0psubN  39750  atpsubN  39754  gcdcomnni  41983  gcdnegnni  41984  neggcdnni  41985  60gcd7e1  42000  lcmeprodgcdi  42002  lcm2un  42009  lcm3un  42010  lcmineqlem4  42027  lcmineqlem6  42029  3lexlogpow5ineq1  42049  aks4d1p1p2  42065  mzpclall  42722  diophin  42767  diophun  42768  eldioph4b  42806  irrapx1  42823  2nn0ind  42941  aomclem4  43053  onexlimgt  43239  nnoeomeqom  43308  oaomoencom  43313  oenassex  43314  succlg  43324  dflim5  43325  omabs2  43328  tfsconcatfv2  43336  ifpid3g  43488  ifpid2g  43489  ifpbi1b  43499  eu0  43516  pwinfi  43560  rtrclex  43613  cnvrcl0  43621  dfrcl2  43670  relexp1idm  43710  relexp0idm  43711  clsk1independent  44042  lhe4.4ex1a  44325  expgrowth  44331  ax6e2nd  44555  uun0.1  44774  relopabVD  44897  ax6e2ndVD  44904  sb5ALTVD  44909  ax6e2ndALT  44926  permaxinf2lem  45009  rexanuz2nf  45495  dvmptconst  45920  dvmptidg  45922  dvmulcncf  45930  dvdivcncf  45932  dvnprodlem3  45953  itgsinexplem1  45959  volioof  45992  stoweidlem13  46018  stoweidlem14  46019  stoweidlem26  46031  stoweidlem34  46039  stoweidlem49  46054  stoweidlem59  46064  dirkertrigeqlem3  46105  dirkercncflem1  46108  dirkercncflem2  46109  fourierdlem57  46168  fourierdlem62  46173  fourierdlem103  46214  fourierdlem111  46222  fourierswlem  46235  fouriersw  46236  salexct2  46344  salexct3  46347  salgencntex  46348  salgensscntex  46349  gsumge0cl  46376  sge00  46381  sge0tsms  46385  0ome  46534  ovnlecvr  46563  ovn0lem  46570  hoidmvle  46605  ovnsubadd2lem  46650  smflimlem6  46781  mbfpsssmf  46788  smfmullem4  46799  smfpimbor1lem1  46803  astbstanbst  46914  aistbistaandb  46915  abnotataxb  46921  aifftbifffaibif  46926  confun4  46947  plcofph  46949  plvcofph  46951  plvcofphax  46952  plvofpos  46953  mdandyv0  46954  mdandyv1  46955  mdandyv2  46956  mdandyv3  46957  mdandyv4  46958  mdandyv5  46959  mdandyv6  46960  mdandyv7  46961  mdandyv8  46962  mdandyv9  46963  mdandyv10  46964  mdandyv11  46965  mdandyv12  46966  mdandyv13  46967  mdandyv14  46968  mdandyv15  46969  mdandyvr0  46970  mdandyvr1  46971  mdandyvr2  46972  mdandyvr3  46973  mdandyvr4  46974  mdandyvr5  46975  mdandyvr6  46976  mdandyvr7  46977  mdandyvrx0  46986  mdandyvrx1  46987  mdandyvrx2  46988  mdandyvrx3  46989  mdandyvrx4  46990  mdandyvrx5  46991  mdandyvrx6  46992  mdandyvrx7  46993  dandysum2p2e4  47003  or2expropbilem1  47037  dfnelbr2  47278  2ltceilhalf  47333  ich2exprop  47476  paireqne  47516  fmtno4prmfac  47577  31prm  47602  lighneallem4a  47613  41prothprmlem2  47623  zofldiv2ALTV  47667  nfermltl8rev  47747  nfermltl2rev  47748  nfermltlrev  47749  gbegt5  47766  gbowgt5  47767  gboge9  47769  9gbo  47779  11gbo  47780  nnsum3primes4  47793  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  tgblthelfgott  47820  tgoldbach  47822  ushggricedg  47931  isubgrgrim  47933  stgrvtx  47957  stgriedg  47958  stgrusgra  47962  stgr1  47964  uspgrlim  47995  clnbgr3stgrgrlic  48015  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  gpgvtx  48038  gpgiedg  48039  gpgorder  48054  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedgiov  48060  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg3kgrtriexlem3  48080  gpg3kgrtriexlem6  48083  gpgprismgr4cycllem2  48090  gpgprismgr4cyclex  48101  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  pgnbgreunbgrlem6  48118  gpg5ngric  48122  nn0mnd  48171  mgmplusgiopALT  48186  sgrp2sgrp  48220  2zrngaabl  48242  funcringcsetcALTV2lem8  48289  funcringcsetclem8ALTV  48312  zlmodzxzlmod  48346  zlmodzxzel  48347  zlmodzxzscm  48349  zlmodzxzadd  48350  snlindsntorlem  48463  ldepspr  48466  lmod1lem2  48481  lmod1lem3  48482  lmod1lem4  48483  lmod1lem5  48484  lmodn0  48488  zlmodzxznm  48490  zlmodzxzldeplem  48491  zlmodzxzldeplem1  48493  zlmodzxzldeplem3  48495  lvecpsslmod  48500  ldepsnlinc  48501  ldepslinc  48502  expnegico01  48511  zofldiv2  48524  flnn0div2ge  48526  elbigo2  48545  nnlog2ge0lt1  48559  digfval  48590  dignnld  48596  dignn0flhalf  48611  2arymaptfo  48647  itcovalt2lem1  48668  prelrrx2  48706  eenglngeehlnmlem2  48731  rrxsphere  48741  line2  48745  line2x  48747  line2y  48748  itsclc0yqsollem2  48756  inlinecirc02plem  48779  sepfsepc  48920  invfn  49023  alimp-surprise  49773  aacllem  49794