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 206  df-an 396

This theorem is referenced by:  mp4an  689  pm4.87  839  3pm3.2i  1337  unssi  4115  ssini  4162  opthhausdorff  5425  elvv  5652  relopabiv  5719  relopabi  5721  dfpo2  6188  funpr  6474  funcnvpr  6480  mpov  7364  caovcom  7447  snnex  7586  pwnex  7587  1st2val  7832  2nd2val  7833  elxp7  7839  opreuopreu  7849  mptmpoopabbrd  7894  wfrlem13OLD  8123  wfr3OLD  8140  tfr1a  8196  oeoa  8390  oeoe  8392  erov  8561  endisj  8799  phplem2  8893  snopfsupp  9081  r1funlim  9455  dfac2b  9817  cflecard  9940  canth4  10334  canthnumlem  10335  canthwelem  10337  canthp1lem2  10340  pwfseqlem4  10349  wunex3  10428  addsrpr  10762  mulsrpr  10763  recexsrlem  10790  mulcani  11544  div1  11594  recdiv  11611  divdiv1  11616  divdiv2  11617  div23i  11663  div11i  11664  divmuldivi  11665  divadddivi  11667  divdivdivi  11668  lemulge11  11767  negiso  11885  dfnn3  11917  2cnne0  12113  2rene0  12114  halfpm6th  12124  avglt1  12141  avglt2  12142  div4p1lem1div2  12158  3halfnz  12329  divlt1lt  12728  divle1le  12729  nnledivrp  12771  x2times  12962  xrsupsslem  12970  xrinfmsslem  12971  fz0to4untppr  13288  om2uzoi  13603  fzennn  13616  expge1  13748  sqoddm1div8  13886  faclbnd2  13933  faclbnd4lem1  13935  4bc2eq6  13971  hashfxnn0  13979  hashsnlei  14061  hashunlei  14068  hashsslei  14069  hash2prb  14114  repswccat  14427  cshwsexa  14465  funcnvs4  14556  f1oun2prg  14558  wrdlen2i  14583  relexpaddg  14692  cjreb  14762  sqrt2gt1lt2  14914  abs1m  14975  bpoly3  15696  ege2le3  15727  efi4p  15774  efival  15789  sin01bnd  15822  cos01bnd  15823  cos1bnd  15824  cos2bnd  15825  sin01gt0  15827  cos01gt0  15828  sin02gt0  15829  sincos2sgn  15831  sin4lt0  15832  egt2lt3  15843  rpnnen2lem3  15853  rpnnen2lem11  15861  nthruc  15889  nthruz  15890  3dvdsdec  15969  3dvds2dec  15970  mod2eq1n2dvds  15984  halfleoddlt  15999  divalglem5  16034  ndvdsi  16049  flodddiv4  16050  flodddiv4lt  16052  bitsp1o  16068  3lcm2e6woprm  16248  6lcm4e12  16249  pcrec  16487  prmrec  16551  prmgaplcmlem1  16680  prmgaplcm  16689  modsubi  16701  structfn  16785  strleun  16786  isofn  17404  sscres  17452  funcestrcsetclem7  17779  funcestrcsetclem8  17780  fullestrcsetc  17784  mgmnsgrpex  18485  pwmnd  18491  ga0  18819  symg2bas  18915  f1otrspeq  18970  psgnsn  19043  0frgp  19300  gsummptnn0fz  19502  srgbinomlem4  19694  cnfldfun  20522  cnfldfunALT  20523  cnfld1  20535  cnsubdrglem  20561  expmhm  20579  expghm  20609  psrbag0  21180  psrbagsn  21181  coe1fsupp  21295  coe1mul2  21350  evls1sca  21399  matmulr  21495  mat1dimelbas  21528  mat1f1o  21535  m2detleib  21688  smadiadetglem1  21728  pmatcollpw3fi1lem2  21844  cpmidpmatlem2  21928  cpmadumatpolylem1  21938  cayhamlem3  21944  cayhamlem4  21945  isbasis3g  22007  fctop  22062  cctop  22064  refref  22572  bl2in  23461  dscmet  23634  iihalf1  24000  iihalf2  24002  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  iscvsi  24198  zclmncvs  24217  ncvs1  24226  ehl2eudis  24491  minveclem2  24495  minveclem4  24501  ovolunlem1a  24565  volf  24598  i1f1lem  24758  mbfi1fseqlem5  24789  dveflem  25048  pilem2  25516  pilem3  25517  sinhalfpilem  25525  sincosq1lem  25559  tangtx  25567  sinq12gt0  25569  sincos4thpi  25575  sincos6thpi  25577  sincos3rdpi  25578  pigt3  25579  pige3ALT  25581  coseq1  25586  efeq1  25589  efif1olem4  25606  angneg  25858  ang180lem1  25864  1cubrlem  25896  quart1  25911  log2cnv  25999  log2tlbnd  26000  log2ublem1  26001  log2ub  26004  emcllem1  26050  emcllem6  26055  basellem1  26135  basellem2  26136  basellem3  26137  basellem8  26142  ppiublem1  26255  ppiublem2  26256  ppiub  26257  chtublem  26264  chtub  26265  bcmono  26330  bclbnd  26333  bpos1lem  26335  bposlem1  26337  bposlem2  26338  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem6  26342  bposlem7  26343  bposlem8  26344  bposlem9  26345  lgsdir2lem1  26378  1lgs  26393  gausslemma2dlem0c  26411  gausslemma2dlem0d  26412  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  gausslemma2dlem3  26421  gausslemma2dlem5  26424  gausslemma2dlem6  26425  lgsquad2lem2  26438  2lgslem1a1  26442  2lgslem1a2  26443  2lgslem1c  26446  2lgslem3a  26449  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2lgslem3  26457  2lgsoddprmlem1  26461  addsqrexnreu  26495  addsqnreup  26496  chebbnd1lem1  26522  chebbnd1lem3  26524  chebbnd1  26525  dchrisum0flblem2  26562  dchrisum0lem1  26569  mulog2sumlem2  26588  selberglem2  26599  chpdifbndlem1  26606  slotsinbpsd  26707  slotslnbpsd  26708  ercgrg  26782  axlowdimlem4  27216  axlowdimlem5  27217  axlowdimlem6  27218  axlowdimlem7  27219  axlowdimlem8  27220  axlowdimlem10  27222  axlowdimlem11  27223  graop  27302  grastruct  27303  uhgrunop  27348  upgrop  27367  upgrunop  27392  umgrunop  27394  usgrop  27436  usgr2v1e2w  27522  usgrexmpldifpr  27528  usgrexmpledg  27532  uhgrsubgrself  27550  uhgrspan1lem1  27570  upgrres1lem1  27579  fusgrfis  27600  vtxd0nedgb  27758  p1evtxdeqlem  27782  p1evtxdeq  27783  p1evtxdp1  27784  umgr2v2e  27795  vdegp1bi  27807  wlkcomp  27900  upgr2pthnlp  28001  usgr2trlncl  28029  usgr2pthlem  28032  clwlkcomp  28048  uspgrn2crct  28074  wwlksonvtx  28121  wspthnonp  28125  2wlkond  28203  2pthond  28208  2pthon3v  28209  umgr2adedgwlkonALT  28213  umgr2wlk  28215  umgr2wlkon  28216  wpthswwlks2on  28227  elwspths2spth  28233  0ewlk  28379  0pth  28390  0pthonv  28394  1pthon2v  28418  3wlkdlem4  28427  3trlond  28438  3pthond  28440  3spthond  28442  trlsegvdeglem3  28487  eupthvdres  28500  eupth2lemb  28502  ex-natded5.2i  28671  ex-an  28687  ex-id  28699  ex-po  28700  ex-fl  28712  ex-mod  28714  ex-exp  28715  ex-lcm  28723  nvz0  28931  ipidsq  28973  ipdirilem  29092  siilem1  29114  minvecolem2  29138  minvecolem3  29139  minvecolem4  29143  hvsubcan  29337  hvsubcan2  29338  normlem7tALT  29382  helch  29506  hsn0elch  29511  hhshsslem2  29531  hhsssh  29532  shscli  29580  shintcli  29592  shintcl  29593  chintcli  29594  chintcl  29595  shincli  29625  shsval2i  29650  omlsi  29667  chincli  29723  chabs1  29779  fh1i  29884  fh2i  29885  cm2ji  29888  pjnormi  29984  nmopsetn0  30128  nmfnsetn0  30141  lnophm  30282  nmcexi  30289  nmbdfnlb  30313  imaelshi  30321  nlelshi  30323  nmopadjlem  30352  nmopcoadji  30364  hmopidmch  30416  hmopidmpj  30417  sto1i  30499  stlei  30503  stji1i  30505  csmdsymi  30597  chirred  30658  cdj3lem1  30697  rpdp2cl  31058  dp2lt10  31060  dp2lt  31061  dp2ltc  31063  dpfrac1  31068  dplti  31081  dpgti  31082  dpexpp1  31084  dpadd3  31088  dpmul  31089  dpmul4  31090  xrsclat  31191  nn0archi  31449  lmatfvlem  31667  xrge0iifmhm  31791  qqh0  31834  qqh1  31835  rerrext  31859  cnrrext  31860  prsiga  31999  oms0  32164  coinfliprv  32349  ballotlem1  32353  ballotth  32404  signsw0g  32435  hgt750lemd  32528  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  tgoldbachgt  32543  subfacval2  33049  erdszelem2  33054  cvmliftlem4  33150  satom  33218  satfv1  33225  sat1el2xp  33241  fmlaomn0  33252  satfdmfmla  33262  satfv1fvfmla1  33285  ex-sategoelelomsuc  33288  ex-sategoelel12  33289  prv0  33292  prv1n  33293  elmrsubrn  33382  msubfval  33386  problem4  33526  quad3  33528  br6  33630  dfon2lem3  33667  ssttrcl  33701  ttrclselem2  33712  poxp2  33717  poseq  33729  fullfunfnv  34175  fneref  34466  filnetlem2  34495  filnetlem3  34496  onpsstopbas  34546  dnizeq0  34582  dnibndlem12  34596  knoppcnlem5  34604  knoppcnlem8  34607  knoppcnlem10  34609  knoppcnlem11  34610  knoppndvlem14  34632  cnndvlem1  34644  bj-genr  34715  bj-genl  34716  bj-genan  34717  bj-2upln1upl  35141  bj-vtoclgfALT  35157  bj-brab2a1  35247  bj-opabssvv  35248  taupilem1  35419  topdifinf  35447  sin2h  35694  cos2h  35695  tan2h  35696  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem29  35733  poimirlem31  35735  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2addnclem2  35756  asindmre  35787  heiborlem7  35902  riscer  36073  refrelcoss3  36508  symrelcoss3  36510  ishlatiN  37296  0psubN  37690  atpsubN  37694  gcdcomnni  39925  gcdnegnni  39926  neggcdnni  39927  60gcd7e1  39941  lcmeprodgcdi  39943  lcm2un  39950  lcm3un  39951  lcmineqlem4  39968  lcmineqlem6  39970  3lexlogpow5ineq1  39990  aks4d1p1p2  40006  mzpclall  40465  diophin  40510  diophun  40511  eldioph4b  40549  irrapx1  40566  2nn0ind  40683  aomclem4  40798  ifpid3g  40997  ifpid2g  40998  ifpbi1b  41008  eu0  41025  pwinfi  41060  rtrclex  41114  cnvrcl0  41122  dfrcl2  41171  relexp1idm  41211  relexp0idm  41212  clsk1independent  41545  lhe4.4ex1a  41836  expgrowth  41842  ax6e2nd  42067  uun0.1  42287  relopabVD  42410  ax6e2ndVD  42417  sb5ALTVD  42422  ax6e2ndALT  42439  dvmptconst  43346  dvmptidg  43348  dvmulcncf  43356  dvdivcncf  43358  dvnprodlem3  43379  itgsinexplem1  43385  volioof  43418  stoweidlem13  43444  stoweidlem14  43445  stoweidlem26  43457  stoweidlem34  43465  stoweidlem49  43480  stoweidlem59  43490  dirkertrigeqlem3  43531  dirkercncflem1  43534  dirkercncflem2  43535  fourierdlem57  43594  fourierdlem62  43599  fourierdlem103  43640  fourierdlem111  43648  fourierswlem  43661  fouriersw  43662  salexct2  43768  salexct3  43771  salgencntex  43772  salgensscntex  43773  gsumge0cl  43799  sge00  43804  sge0tsms  43808  0ome  43957  ovnlecvr  43986  ovn0lem  43993  hoidmvle  44028  ovnsubadd2lem  44073  smflimlem6  44198  mbfpsssmf  44205  smfmullem4  44215  smfpimbor1lem1  44219  astbstanbst  44291  aistbistaandb  44292  abnotataxb  44298  aifftbifffaibif  44303  confun4  44324  plcofph  44326  plvcofph  44328  plvcofphax  44329  plvofpos  44330  mdandyv0  44331  mdandyv1  44332  mdandyv2  44333  mdandyv3  44334  mdandyv4  44335  mdandyv5  44336  mdandyv6  44337  mdandyv7  44338  mdandyv8  44339  mdandyv9  44340  mdandyv10  44341  mdandyv11  44342  mdandyv12  44343  mdandyv13  44344  mdandyv14  44345  mdandyv15  44346  mdandyvr0  44347  mdandyvr1  44348  mdandyvr2  44349  mdandyvr3  44350  mdandyvr4  44351  mdandyvr5  44352  mdandyvr6  44353  mdandyvr7  44354  mdandyvrx0  44363  mdandyvrx1  44364  mdandyvrx2  44365  mdandyvrx3  44366  mdandyvrx4  44367  mdandyvrx5  44368  mdandyvrx6  44369  mdandyvrx7  44370  dandysum2p2e4  44380  or2expropbilem1  44413  dfnelbr2  44652  ich2exprop  44811  paireqne  44851  fmtno4prmfac  44912  31prm  44937  lighneallem4a  44948  41prothprmlem2  44958  zofldiv2ALTV  45002  nfermltl8rev  45082  nfermltl2rev  45083  nfermltlrev  45084  gbegt5  45101  gbowgt5  45102  gboge9  45104  9gbo  45114  11gbo  45115  nnsum3primes4  45128  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  tgblthelfgott  45155  tgoldbach  45157  isomgrref  45175  ushrisomgr  45181  nn0mnd  45261  mgmplusgiopALT  45276  sgrp2sgrp  45310  isrnghm  45338  2zrngaabl  45390  rnghmsscmap2  45419  rnghmsscmap  45420  funcrngcsetc  45444  funcrngcsetcALT  45445  rhmsscmap2  45465  rhmsscmap  45466  funcringcsetc  45481  funcringcsetcALTV2lem8  45489  funcringcsetclem8ALTV  45512  zlmodzxzlmod  45578  zlmodzxzel  45579  zlmodzxzscm  45581  zlmodzxzadd  45582  snlindsntorlem  45699  ldepspr  45702  lmod1lem2  45717  lmod1lem3  45718  lmod1lem4  45719  lmod1lem5  45720  lmodn0  45724  zlmodzxznm  45726  zlmodzxzldeplem  45727  zlmodzxzldeplem1  45729  zlmodzxzldeplem3  45731  lvecpsslmod  45736  ldepsnlinc  45737  ldepslinc  45738  expnegico01  45747  zofldiv2  45765  flnn0div2ge  45767  elbigo2  45786  nnlog2ge0lt1  45800  digfval  45831  dignnld  45837  dignn0flhalf  45852  2arymaptfo  45888  itcovalt2lem1  45909  prelrrx2  45947  eenglngeehlnmlem2  45972  rrxsphere  45982  line2  45986  line2x  45988  line2y  45989  itsclc0yqsollem2  45997  inlinecirc02plem  46020  sepfsepc  46109  alimp-surprise  46370  aacllem  46391