Theorem pm3.2i 472

Description: Infer conjunction of premises. Inference associated with pm3.2 471. Its associated deduction is jca 513 (and the double deduction is jcad 514). (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 471	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 397

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 398

This theorem is referenced by:  mp4an  692  pm4.87  842  3pm3.2i  1340  unssi  4185  ssini  4231  opthhausdorff  5517  elvv  5749  elopaelxp  5764  relopabiv  5819  relopabi  5821  dfpo2  6293  funpr  6602  funcnvpr  6608  mpov  7517  caovcom  7601  snnex  7742  pwnex  7743  1st2val  8000  2nd2val  8001  elxp7  8007  opreuopreu  8017  mptmpoopabbrdOLD  8066  poxp2  8126  poseq  8141  wfrlem13OLD  8318  wfr3OLD  8335  tfr1a  8391  oeoa  8594  oeoe  8596  erov  8805  endisj  9055  phplem2OLD  9215  snopfsupp  9383  ssttrcl  9707  ttrclselem2  9718  r1funlim  9758  dfac2b  10122  cflecard  10245  canth4  10639  canthnumlem  10640  canthwelem  10642  canthp1lem2  10645  pwfseqlem4  10654  wunex3  10733  addsrpr  11067  mulsrpr  11068  recexsrlem  11095  mulcani  11850  div1  11900  recdiv  11917  divdiv1  11922  divdiv2  11923  div23i  11969  div11i  11970  divmuldivi  11971  divadddivi  11973  divdivdivi  11974  lemulge11  12073  negiso  12191  dfnn3  12223  2cnne0  12419  2rene0  12420  halfpm6th  12430  avglt1  12447  avglt2  12448  div4p1lem1div2  12464  3halfnz  12638  divlt1lt  13040  divle1le  13041  nnledivrp  13083  x2times  13275  xrsupsslem  13283  xrinfmsslem  13284  fz0to4untppr  13601  om2uzoi  13917  fzennn  13930  expge1  14062  sqoddm1div8  14203  faclbnd2  14248  faclbnd4lem1  14250  4bc2eq6  14286  hashfxnn0  14294  hashsnlei  14375  hashunlei  14382  hashsslei  14383  hash2prb  14430  repswccat  14733  cshwsexaOLD  14772  funcnvs4  14863  f1oun2prg  14865  wrdlen2i  14890  relexpaddg  14997  cjreb  15067  sqrt2gt1lt2  15218  abs1m  15279  bpoly3  15999  ege2le3  16030  efi4p  16077  efival  16092  sin01bnd  16125  cos01bnd  16126  cos1bnd  16127  cos2bnd  16128  sin01gt0  16130  cos01gt0  16131  sin02gt0  16132  sincos2sgn  16134  sin4lt0  16135  egt2lt3  16146  rpnnen2lem3  16156  rpnnen2lem11  16164  nthruc  16192  nthruz  16193  3dvdsdec  16272  3dvds2dec  16273  mod2eq1n2dvds  16287  halfleoddlt  16302  divalglem5  16337  ndvdsi  16352  flodddiv4  16353  flodddiv4lt  16355  bitsp1o  16371  3lcm2e6woprm  16549  6lcm4e12  16550  pcrec  16788  prmrec  16852  prmgaplcmlem1  16981  prmgaplcm  16990  modsubi  17002  structfn  17086  strleun  17087  slotsdifipndx  17277  slotsdifplendx  17317  slotsdifdsndx  17336  slotsdifunifndx  17343  slotsdifplendx2  17359  slotsdifocndx  17360  isofn  17719  sscres  17767  funcestrcsetclem7  18095  funcestrcsetclem8  18096  fullestrcsetc  18100  mgmnsgrpex  18809  pwmnd  18815  ga0  19157  symg2bas  19255  f1otrspeq  19310  psgnsn  19383  0frgp  19642  gsummptnn0fz  19849  srgbinomlem4  20046  cnfldfun  20949  cnfldfunALT  20950  cnfldfunALTOLD  20951  cnfld1  20963  cnsubdrglem  20989  expmhm  21007  expghm  21037  psrbag0  21615  psrbagsn  21616  coe1fsupp  21730  coe1mul2  21783  evls1sca  21834  matmulr  21932  mat1dimelbas  21965  mat1f1o  21972  m2detleib  22125  smadiadetglem1  22165  pmatcollpw3fi1lem2  22281  cpmidpmatlem2  22365  cpmadumatpolylem1  22375  cayhamlem3  22381  cayhamlem4  22382  isbasis3g  22444  fctop  22499  cctop  22501  refref  23009  bl2in  23898  dscmet  24073  iihalf1  24439  iihalf2  24441  icopnfhmeo  24451  iccpnfhmeo  24453  xrhmeo  24454  iscvsi  24637  zclmncvs  24657  ncvs1  24666  ehl2eudis  24931  minveclem2  24935  minveclem4  24941  ovolunlem1a  25005  volf  25038  i1f1lem  25198  mbfi1fseqlem5  25229  dveflem  25488  pilem2  25956  pilem3  25957  sinhalfpilem  25965  sincosq1lem  25999  tangtx  26007  sinq12gt0  26009  sincos4thpi  26015  sincos6thpi  26017  sincos3rdpi  26018  pigt3  26019  pige3ALT  26021  coseq1  26026  efeq1  26029  efif1olem4  26046  angneg  26298  ang180lem1  26304  1cubrlem  26336  quart1  26351  log2cnv  26439  log2tlbnd  26440  log2ublem1  26441  log2ub  26444  emcllem1  26490  emcllem6  26495  basellem1  26575  basellem2  26576  basellem3  26577  basellem8  26582  ppiublem1  26695  ppiublem2  26696  ppiub  26697  chtublem  26704  chtub  26705  bcmono  26770  bclbnd  26773  bpos1lem  26775  bposlem1  26777  bposlem2  26778  bposlem3  26779  bposlem4  26780  bposlem5  26781  bposlem6  26782  bposlem7  26783  bposlem8  26784  bposlem9  26785  lgsdir2lem1  26818  1lgs  26833  gausslemma2dlem0c  26851  gausslemma2dlem0d  26852  gausslemma2dlem1a  26858  gausslemma2dlem2  26860  gausslemma2dlem3  26861  gausslemma2dlem5  26864  gausslemma2dlem6  26865  lgsquad2lem2  26878  2lgslem1a1  26882  2lgslem1a2  26883  2lgslem1c  26886  2lgslem3a  26889  2lgslem3b  26890  2lgslem3c  26891  2lgslem3d  26892  2lgslem3  26897  2lgsoddprmlem1  26901  addsqrexnreu  26935  addsqnreup  26936  chebbnd1lem1  26962  chebbnd1lem3  26964  chebbnd1  26965  dchrisum0flblem2  27002  dchrisum0lem1  27009  mulog2sumlem2  27028  selberglem2  27039  chpdifbndlem1  27046  mulscl  27580  sltmul  27582  divs1  27641  precsexlem8  27650  slotsinbpsd  27682  slotslnbpsd  27683  ercgrg  27758  axlowdimlem4  28193  axlowdimlem5  28194  axlowdimlem6  28195  axlowdimlem7  28196  axlowdimlem8  28197  axlowdimlem10  28199  axlowdimlem11  28200  graop  28279  grastruct  28280  uhgrunop  28325  upgrop  28344  upgrunop  28369  umgrunop  28371  usgrop  28413  usgr2v1e2w  28499  usgrexmpldifpr  28505  usgrexmpledg  28509  uhgrsubgrself  28527  uhgrspan1lem1  28547  upgrres1lem1  28556  fusgrfis  28577  vtxd0nedgb  28735  p1evtxdeqlem  28759  p1evtxdeq  28760  p1evtxdp1  28761  umgr2v2e  28772  vdegp1bi  28784  wlkcomp  28878  upgr2pthnlp  28979  usgr2trlncl  29007  usgr2pthlem  29010  clwlkcomp  29026  uspgrn2crct  29052  wwlksonvtx  29099  wspthnonp  29103  2wlkond  29181  2pthond  29186  2pthon3v  29187  umgr2adedgwlkonALT  29191  umgr2wlk  29193  umgr2wlkon  29194  wpthswwlks2on  29205  elwspths2spth  29211  0ewlk  29357  0pth  29368  0pthonv  29372  1pthon2v  29396  3wlkdlem4  29405  3trlond  29416  3pthond  29418  3spthond  29420  trlsegvdeglem3  29465  eupthvdres  29478  eupth2lemb  29480  ex-natded5.2i  29649  ex-an  29665  ex-id  29677  ex-po  29678  ex-fl  29690  ex-mod  29692  ex-exp  29693  ex-lcm  29701  nvz0  29909  ipidsq  29951  ipdirilem  30070  siilem1  30092  minvecolem2  30116  minvecolem3  30117  minvecolem4  30121  hvsubcan  30315  hvsubcan2  30316  normlem7tALT  30360  helch  30484  hsn0elch  30489  hhshsslem2  30509  hhsssh  30510  shscli  30558  shintcli  30570  shintcl  30571  chintcli  30572  chintcl  30573  shincli  30603  shsval2i  30628  omlsi  30645  chincli  30701  chabs1  30757  fh1i  30862  fh2i  30863  cm2ji  30866  pjnormi  30962  nmopsetn0  31106  nmfnsetn0  31119  lnophm  31260  nmcexi  31267  nmbdfnlb  31291  imaelshi  31299  nlelshi  31301  nmopadjlem  31330  nmopcoadji  31342  hmopidmch  31394  hmopidmpj  31395  sto1i  31477  stlei  31481  stji1i  31483  csmdsymi  31575  chirred  31636  cdj3lem1  31675  rpdp2cl  32036  dp2lt10  32038  dp2lt  32039  dp2ltc  32041  dpfrac1  32046  dplti  32059  dpgti  32060  dpexpp1  32062  dpadd3  32066  dpmul  32067  dpmul4  32068  xrsclat  32169  nn0archi  32451  lmatfvlem  32784  xrge0iifmhm  32908  qqh0  32953  qqh1  32954  rerrext  32978  cnrrext  32979  prsiga  33118  oms0  33285  coinfliprv  33470  ballotlem1  33474  ballotth  33525  signsw0g  33556  hgt750lemd  33649  hgt750lem  33652  hgt750lem2  33653  hgt750leme  33659  tgoldbachgt  33664  subfacval2  34167  erdszelem2  34172  cvmliftlem4  34268  satom  34336  satfv1  34343  sat1el2xp  34359  fmlaomn0  34370  satfdmfmla  34380  satfv1fvfmla1  34403  ex-sategoelelomsuc  34406  ex-sategoelel12  34407  prv0  34410  prv1n  34411  elmrsubrn  34500  msubfval  34504  problem4  34642  quad3  34644  br6  34716  dfon2lem3  34746  fullfunfnv  34907  fneref  35224  filnetlem2  35253  filnetlem3  35254  onpsstopbas  35304  dnizeq0  35340  dnibndlem12  35354  knoppcnlem5  35362  knoppcnlem8  35365  knoppcnlem10  35367  knoppcnlem11  35368  knoppndvlem14  35390  cnndvlem1  35402  bj-genr  35473  bj-genl  35474  bj-genan  35475  bj-2upln1upl  35894  bj-vtoclgfALT  35929  bj-brab2a1  36019  bj-opabssvv  36020  taupilem1  36191  topdifinf  36219  sin2h  36467  cos2h  36468  tan2h  36469  poimirlem1  36478  poimirlem2  36479  poimirlem3  36480  poimirlem4  36481  poimirlem6  36483  poimirlem7  36484  poimirlem11  36488  poimirlem12  36489  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem22  36499  poimirlem23  36500  poimirlem24  36501  poimirlem25  36502  poimirlem26  36503  poimirlem29  36506  poimirlem31  36508  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2addnclem2  36529  asindmre  36560  heiborlem7  36674  riscer  36845  refrelcoss3  37322  symrelcoss3  37324  ishlatiN  38214  0psubN  38609  atpsubN  38613  gcdcomnni  40843  gcdnegnni  40844  neggcdnni  40845  60gcd7e1  40859  lcmeprodgcdi  40861  lcm2un  40868  lcm3un  40869  lcmineqlem4  40886  lcmineqlem6  40888  3lexlogpow5ineq1  40908  aks4d1p1p2  40924  mzpclall  41451  diophin  41496  diophun  41497  eldioph4b  41535  irrapx1  41552  2nn0ind  41670  aomclem4  41785  onexlimgt  41978  nnoeomeqom  42048  oaomoencom  42053  oenassex  42054  succlg  42064  dflim5  42065  omabs2  42068  tfsconcatfv2  42076  ifpid3g  42229  ifpid2g  42230  ifpbi1b  42240  eu0  42257  pwinfi  42301  rtrclex  42354  cnvrcl0  42362  dfrcl2  42411  relexp1idm  42451  relexp0idm  42452  clsk1independent  42783  lhe4.4ex1a  43074  expgrowth  43080  ax6e2nd  43305  uun0.1  43525  relopabVD  43648  ax6e2ndVD  43655  sb5ALTVD  43660  ax6e2ndALT  43677  rexanuz2nf  44190  dvmptconst  44618  dvmptidg  44620  dvmulcncf  44628  dvdivcncf  44630  dvnprodlem3  44651  itgsinexplem1  44657  volioof  44690  stoweidlem13  44716  stoweidlem14  44717  stoweidlem26  44729  stoweidlem34  44737  stoweidlem49  44752  stoweidlem59  44762  dirkertrigeqlem3  44803  dirkercncflem1  44806  dirkercncflem2  44807  fourierdlem57  44866  fourierdlem62  44871  fourierdlem103  44912  fourierdlem111  44920  fourierswlem  44933  fouriersw  44934  salexct2  45042  salexct3  45045  salgencntex  45046  salgensscntex  45047  gsumge0cl  45074  sge00  45079  sge0tsms  45083  0ome  45232  ovnlecvr  45261  ovn0lem  45268  hoidmvle  45303  ovnsubadd2lem  45348  smflimlem6  45479  mbfpsssmf  45486  smfmullem4  45497  smfpimbor1lem1  45501  astbstanbst  45606  aistbistaandb  45607  abnotataxb  45613  aifftbifffaibif  45618  confun4  45639  plcofph  45641  plvcofph  45643  plvcofphax  45644  plvofpos  45645  mdandyv0  45646  mdandyv1  45647  mdandyv2  45648  mdandyv3  45649  mdandyv4  45650  mdandyv5  45651  mdandyv6  45652  mdandyv7  45653  mdandyv8  45654  mdandyv9  45655  mdandyv10  45656  mdandyv11  45657  mdandyv12  45658  mdandyv13  45659  mdandyv14  45660  mdandyv15  45661  mdandyvr0  45662  mdandyvr1  45663  mdandyvr2  45664  mdandyvr3  45665  mdandyvr4  45666  mdandyvr5  45667  mdandyvr6  45668  mdandyvr7  45669  mdandyvrx0  45678  mdandyvrx1  45679  mdandyvrx2  45680  mdandyvrx3  45681  mdandyvrx4  45682  mdandyvrx5  45683  mdandyvrx6  45684  mdandyvrx7  45685  dandysum2p2e4  45695  or2expropbilem1  45729  dfnelbr2  45968  ich2exprop  46126  paireqne  46166  fmtno4prmfac  46227  31prm  46252  lighneallem4a  46263  41prothprmlem2  46273  zofldiv2ALTV  46317  nfermltl8rev  46397  nfermltl2rev  46398  nfermltlrev  46399  gbegt5  46416  gbowgt5  46417  gboge9  46419  9gbo  46429  11gbo  46430  nnsum3primes4  46443  nnsum3primesgbe  46447  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  tgblthelfgott  46470  tgoldbach  46472  isomgrref  46490  ushrisomgr  46496  nn0mnd  46576  mgmplusgiopALT  46591  sgrp2sgrp  46625  isrnghm  46676  2zrngaabl  46796  rnghmsscmap2  46825  rnghmsscmap  46826  funcrngcsetc  46850  funcrngcsetcALT  46851  rhmsscmap2  46871  rhmsscmap  46872  funcringcsetc  46887  funcringcsetcALTV2lem8  46895  funcringcsetclem8ALTV  46918  zlmodzxzlmod  46984  zlmodzxzel  46985  zlmodzxzscm  46987  zlmodzxzadd  46988  snlindsntorlem  47105  ldepspr  47108  lmod1lem2  47123  lmod1lem3  47124  lmod1lem4  47125  lmod1lem5  47126  lmodn0  47130  zlmodzxznm  47132  zlmodzxzldeplem  47133  zlmodzxzldeplem1  47135  zlmodzxzldeplem3  47137  lvecpsslmod  47142  ldepsnlinc  47143  ldepslinc  47144  expnegico01  47153  zofldiv2  47171  flnn0div2ge  47173  elbigo2  47192  nnlog2ge0lt1  47206  digfval  47237  dignnld  47243  dignn0flhalf  47258  2arymaptfo  47294  itcovalt2lem1  47315  prelrrx2  47353  eenglngeehlnmlem2  47378  rrxsphere  47388  line2  47392  line2x  47394  line2y  47395  itsclc0yqsollem2  47403  inlinecirc02plem  47426  sepfsepc  47514  alimp-surprise  47781  aacllem  47802