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  1338  unssi  4200  ssini  4247  opthhausdorff  5526  elvv  5762  elopaelxp  5777  relopabiv  5832  relopabi  5834  dfpo2  6317  funpr  6623  funcnvpr  6629  mpov  7544  caovcom  7629  snnex  7776  pwnex  7777  1st2val  8040  2nd2val  8041  elxp7  8047  opreuopreu  8057  mptmpoopabbrdOLDOLD  8106  poxp2  8166  poseq  8181  wfrlem13OLD  8359  wfr3OLD  8376  tfr1a  8432  oeoa  8633  oeoe  8635  erov  8852  endisj  9096  phplem2OLD  9252  snopfsupp  9428  ssttrcl  9752  ttrclselem2  9763  r1funlim  9803  dfac2b  10168  cflecard  10290  canth4  10684  canthnumlem  10685  canthwelem  10687  canthp1lem2  10690  pwfseqlem4  10699  wunex3  10778  addsrpr  11112  mulsrpr  11113  recexsrlem  11140  mulcani  11899  div1  11954  recdiv  11970  divdiv1  11975  divdiv2  11976  div23i  12022  div11i  12023  divmuldivi  12024  divadddivi  12026  divdivdivi  12027  lemulge11  12127  negiso  12245  dfnn3  12277  2cnne0  12473  2rene0  12474  halfpm6th  12484  avglt1  12501  avglt2  12502  div4p1lem1div2  12518  3halfnz  12694  divlt1lt  13101  divle1le  13102  nnledivrp  13144  x2times  13337  xrsupsslem  13345  xrinfmsslem  13346  fvf1tp  13825  om2uzoi  13992  fzennn  14005  expge1  14136  sqoddm1div8  14278  faclbnd2  14326  faclbnd4lem1  14328  4bc2eq6  14364  hashfxnn0  14372  hashsnlei  14453  hashunlei  14460  hashsslei  14461  hash2prb  14507  repswccat  14820  cshwsexaOLD  14859  funcnvs4  14950  f1oun2prg  14952  wrdlen2i  14977  s2rn  14998  s3rn  14999  s7rn  15000  relexpaddg  15088  cjreb  15158  sqrt2gt1lt2  15309  abs1m  15370  bpoly3  16090  ege2le3  16122  efi4p  16169  efival  16184  sin01bnd  16217  cos01bnd  16218  cos1bnd  16219  cos2bnd  16220  sin01gt0  16222  cos01gt0  16223  sin02gt0  16224  sincos2sgn  16226  sin4lt0  16227  egt2lt3  16238  rpnnen2lem3  16248  rpnnen2lem11  16256  nthruc  16284  nthruz  16285  3dvdsdec  16365  3dvds2dec  16366  mod2eq1n2dvds  16380  halfleoddlt  16395  divalglem5  16430  ndvdsi  16445  flodddiv4  16448  flodddiv4lt  16450  bitsp1o  16466  3lcm2e6woprm  16648  6lcm4e12  16649  pcrec  16891  prmrec  16955  prmgaplcmlem1  17084  prmgaplcm  17093  modsubi  17105  structfn  17189  strleun  17190  slotsdifipndx  17380  slotsdifplendx  17420  slotsdifdsndx  17439  slotsdifunifndx  17446  slotsdifplendx2  17462  slotsdifocndx  17463  isofn  17822  sscres  17870  funcestrcsetclem7  18201  funcestrcsetclem8  18202  fullestrcsetc  18206  mgmnsgrpex  18956  pwmnd  18962  ga0  19328  symg2bas  19424  f1otrspeq  19479  psgnsn  19552  0frgp  19811  gsummptnn0fz  20018  srgbinomlem4  20246  isrnghm  20457  rnghmsscmap2  20645  rnghmsscmap  20646  funcrngcsetc  20656  funcrngcsetcALT  20657  rhmsscmap2  20674  rhmsscmap  20675  funcringcsetc  20690  cnfldfun  21395  cnfldfunALT  21396  cnfldfunOLD  21408  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  cnfld1  21423  cnfld1OLD  21424  cnsubdrglem  21453  expmhm  21471  expghm  21503  pzriprnglem4  21512  pzriprnglem9  21517  pzriprnglem14  21522  pzriprng1ALT  21524  psrbag0  22103  psrbagsn  22104  coe1fsupp  22231  coe1mul2  22287  evls1sca  22342  matmulr  22459  mat1dimelbas  22492  mat1f1o  22499  m2detleib  22652  smadiadetglem1  22692  pmatcollpw3fi1lem2  22808  cpmidpmatlem2  22892  cpmadumatpolylem1  22902  cayhamlem3  22908  cayhamlem4  22909  isbasis3g  22971  fctop  23026  cctop  23028  refref  23536  bl2in  24425  dscmet  24600  iihalf1  24971  iihalf2  24974  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  iscvsi  25175  zclmncvs  25195  ncvs1  25204  ehl2eudis  25469  minveclem2  25473  minveclem4  25479  ovolunlem1a  25544  volf  25577  i1f1lem  25737  mbfi1fseqlem5  25768  dveflem  26031  pilem2  26510  pilem3  26511  sinhalfpilem  26519  sincosq1lem  26553  tangtx  26561  sinq12gt0  26563  sincos4thpi  26569  sincos6thpi  26572  sincos3rdpi  26573  pigt3  26574  pige3ALT  26576  coseq1  26581  efeq1  26584  efif1olem4  26601  angneg  26860  ang180lem1  26866  1cubrlem  26898  quart1  26913  log2cnv  27001  log2tlbnd  27002  log2ublem1  27003  log2ub  27006  emcllem1  27053  emcllem6  27058  basellem1  27138  basellem2  27139  basellem3  27140  basellem8  27145  ppiublem1  27260  ppiublem2  27261  ppiub  27262  chtublem  27269  chtub  27270  bcmono  27335  bclbnd  27338  bpos1lem  27340  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem7  27348  bposlem8  27349  bposlem9  27350  lgsdir2lem1  27383  1lgs  27398  gausslemma2dlem0c  27416  gausslemma2dlem0d  27417  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  gausslemma2dlem3  27426  gausslemma2dlem5  27429  gausslemma2dlem6  27430  lgsquad2lem2  27443  2lgslem1a1  27447  2lgslem1a2  27448  2lgslem1c  27451  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2lgslem3  27462  2lgsoddprmlem1  27466  addsqrexnreu  27500  addsqnreup  27501  chebbnd1lem1  27527  chebbnd1lem3  27529  chebbnd1  27530  dchrisum0flblem2  27567  dchrisum0lem1  27574  mulog2sumlem2  27593  selberglem2  27604  chpdifbndlem1  27611  mulscl  28174  sltmul  28176  divs1  28243  precsexlem8  28252  nohalf  28421  0reno  28443  slotsinbpsd  28463  slotslnbpsd  28464  ercgrg  28539  axlowdimlem4  28974  axlowdimlem5  28975  axlowdimlem6  28976  axlowdimlem7  28977  axlowdimlem8  28978  axlowdimlem10  28980  axlowdimlem11  28981  graop  29060  grastruct  29061  uhgrunop  29106  upgrop  29125  upgrunop  29150  umgrunop  29152  usgrop  29194  usgr2v1e2w  29283  usgrexmpldifpr  29289  usgrexmpledg  29293  uhgrsubgrself  29311  uhgrspan1lem1  29331  upgrres1lem1  29340  fusgrfis  29361  vtxd0nedgb  29520  p1evtxdeqlem  29544  p1evtxdeq  29545  p1evtxdp1  29546  umgr2v2e  29557  vdegp1bi  29569  wlkcomp  29663  upgr2pthnlp  29764  usgr2trlncl  29792  usgr2pthlem  29795  clwlkcomp  29811  uspgrn2crct  29837  wwlksonvtx  29884  wspthnonp  29888  2wlkond  29966  2pthond  29971  2pthon3v  29972  umgr2adedgwlkonALT  29976  umgr2wlk  29978  umgr2wlkon  29979  wpthswwlks2on  29990  elwspths2spth  29996  0ewlk  30142  0pth  30153  0pthonv  30157  1pthon2v  30181  3wlkdlem4  30190  3trlond  30201  3pthond  30203  3spthond  30205  trlsegvdeglem3  30250  eupthvdres  30263  eupth2lemb  30265  ex-natded5.2i  30434  ex-an  30450  ex-id  30462  ex-po  30463  ex-fl  30475  ex-mod  30477  ex-exp  30478  ex-lcm  30486  nvz0  30696  ipidsq  30738  ipdirilem  30857  siilem1  30879  minvecolem2  30903  minvecolem3  30904  minvecolem4  30908  hvsubcan  31102  hvsubcan2  31103  normlem7tALT  31147  helch  31271  hsn0elch  31276  hhshsslem2  31296  hhsssh  31297  shscli  31345  shintcli  31357  shintcl  31358  chintcli  31359  chintcl  31360  shincli  31390  shsval2i  31415  omlsi  31432  chincli  31488  chabs1  31544  fh1i  31649  fh2i  31650  cm2ji  31653  pjnormi  31749  nmopsetn0  31893  nmfnsetn0  31906  lnophm  32047  nmcexi  32054  nmbdfnlb  32078  imaelshi  32086  nlelshi  32088  nmopadjlem  32117  nmopcoadji  32129  hmopidmch  32181  hmopidmpj  32182  sto1i  32264  stlei  32268  stji1i  32270  csmdsymi  32362  chirred  32423  cdj3lem1  32462  rpdp2cl  32848  dp2lt10  32850  dp2lt  32851  dp2ltc  32853  dpfrac1  32858  dplti  32871  dpgti  32872  dpexpp1  32874  dpadd3  32878  dpmul  32879  dpmul4  32880  xrsclat  32995  nn0archi  33354  zringfrac  33561  lmatfvlem  33775  xrge0iifmhm  33899  qqh0  33946  qqh1  33947  rerrext  33971  cnrrext  33972  prsiga  34111  oms0  34278  coinfliprv  34463  ballotlem1  34467  ballotth  34518  signsw0g  34549  hgt750lemd  34641  hgt750lem  34644  hgt750lem2  34645  hgt750leme  34651  tgoldbachgt  34656  subfacval2  35171  erdszelem2  35176  cvmliftlem4  35272  satom  35340  satfv1  35347  sat1el2xp  35363  fmlaomn0  35374  satfdmfmla  35384  satfv1fvfmla1  35407  ex-sategoelelomsuc  35410  ex-sategoelel12  35411  prv0  35414  prv1n  35415  elmrsubrn  35504  msubfval  35508  problem4  35652  quad3  35654  br6  35736  dfon2lem3  35766  fullfunfnv  35927  itgeq12i  36187  fneref  36332  filnetlem2  36361  filnetlem3  36362  onpsstopbas  36412  dnizeq0  36457  dnibndlem12  36471  knoppcnlem5  36479  knoppcnlem8  36482  knoppcnlem11  36485  knoppndvlem14  36507  cnndvlem1  36519  bj-genr  36588  bj-genl  36589  bj-genan  36590  bj-2upln1upl  37006  bj-vtoclgfALT  37041  bj-brab2a1  37131  bj-opabssvv  37132  taupilem1  37303  topdifinf  37331  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem29  37635  poimirlem31  37637  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnclem2  37658  asindmre  37689  heiborlem7  37803  riscer  37974  refrelcoss3  38444  symrelcoss3  38446  ishlatiN  39336  0psubN  39731  atpsubN  39735  gcdcomnni  41969  gcdnegnni  41970  neggcdnni  41971  60gcd7e1  41986  lcmeprodgcdi  41988  lcm2un  41995  lcm3un  41996  lcmineqlem4  42013  lcmineqlem6  42015  3lexlogpow5ineq1  42035  aks4d1p1p2  42051  mzpclall  42714  diophin  42759  diophun  42760  eldioph4b  42798  irrapx1  42815  2nn0ind  42933  aomclem4  43045  onexlimgt  43231  nnoeomeqom  43301  oaomoencom  43306  oenassex  43307  succlg  43317  dflim5  43318  omabs2  43321  tfsconcatfv2  43329  ifpid3g  43481  ifpid2g  43482  ifpbi1b  43492  eu0  43509  pwinfi  43553  rtrclex  43606  cnvrcl0  43614  dfrcl2  43663  relexp1idm  43703  relexp0idm  43704  clsk1independent  44035  lhe4.4ex1a  44324  expgrowth  44330  ax6e2nd  44555  uun0.1  44775  relopabVD  44898  ax6e2ndVD  44905  sb5ALTVD  44910  ax6e2ndALT  44927  rexanuz2nf  45442  dvmptconst  45870  dvmptidg  45872  dvmulcncf  45880  dvdivcncf  45882  dvnprodlem3  45903  itgsinexplem1  45909  volioof  45942  stoweidlem13  45968  stoweidlem14  45969  stoweidlem26  45981  stoweidlem34  45989  stoweidlem49  46004  stoweidlem59  46014  dirkertrigeqlem3  46055  dirkercncflem1  46058  dirkercncflem2  46059  fourierdlem57  46118  fourierdlem62  46123  fourierdlem103  46164  fourierdlem111  46172  fourierswlem  46185  fouriersw  46186  salexct2  46294  salexct3  46297  salgencntex  46298  salgensscntex  46299  gsumge0cl  46326  sge00  46331  sge0tsms  46335  0ome  46484  ovnlecvr  46513  ovn0lem  46520  hoidmvle  46555  ovnsubadd2lem  46600  smflimlem6  46731  mbfpsssmf  46738  smfmullem4  46749  smfpimbor1lem1  46753  astbstanbst  46858  aistbistaandb  46859  abnotataxb  46865  aifftbifffaibif  46870  confun4  46891  plcofph  46893  plvcofph  46895  plvcofphax  46896  plvofpos  46897  mdandyv0  46898  mdandyv1  46899  mdandyv2  46900  mdandyv3  46901  mdandyv4  46902  mdandyv5  46903  mdandyv6  46904  mdandyv7  46905  mdandyv8  46906  mdandyv9  46907  mdandyv10  46908  mdandyv11  46909  mdandyv12  46910  mdandyv13  46911  mdandyv14  46912  mdandyv15  46913  mdandyvr0  46914  mdandyvr1  46915  mdandyvr2  46916  mdandyvr3  46917  mdandyvr4  46918  mdandyvr5  46919  mdandyvr6  46920  mdandyvr7  46921  mdandyvrx0  46930  mdandyvrx1  46931  mdandyvrx2  46932  mdandyvrx3  46933  mdandyvrx4  46934  mdandyvrx5  46935  mdandyvrx6  46936  mdandyvrx7  46937  dandysum2p2e4  46947  or2expropbilem1  46981  dfnelbr2  47222  ich2exprop  47395  paireqne  47435  fmtno4prmfac  47496  31prm  47521  lighneallem4a  47532  41prothprmlem2  47542  zofldiv2ALTV  47586  nfermltl8rev  47666  nfermltl2rev  47667  nfermltlrev  47668  gbegt5  47685  gbowgt5  47686  gboge9  47688  9gbo  47698  11gbo  47699  nnsum3primes4  47712  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  tgblthelfgott  47739  tgoldbach  47741  ushggricedg  47833  isubgrgrim  47834  stgrvtx  47856  stgriedg  47857  stgrusgra  47861  stgr1  47863  uspgrlim  47894  clnbgr3stgrgrlic  47914  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  gpgvtx  47937  gpgiedg  47938  gpgorder  47947  2ltceilhalf  47949  gpgvtxedg0  47955  gpgvtxedg1  47956  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  nn0mnd  48022  mgmplusgiopALT  48037  sgrp2sgrp  48071  2zrngaabl  48093  funcringcsetcALTV2lem8  48140  funcringcsetclem8ALTV  48163  zlmodzxzlmod  48198  zlmodzxzel  48199  zlmodzxzscm  48201  zlmodzxzadd  48202  snlindsntorlem  48315  ldepspr  48318  lmod1lem2  48333  lmod1lem3  48334  lmod1lem4  48335  lmod1lem5  48336  lmodn0  48340  zlmodzxznm  48342  zlmodzxzldeplem  48343  zlmodzxzldeplem1  48345  zlmodzxzldeplem3  48347  lvecpsslmod  48352  ldepsnlinc  48353  ldepslinc  48354  expnegico01  48363  zofldiv2  48380  flnn0div2ge  48382  elbigo2  48401  nnlog2ge0lt1  48415  digfval  48446  dignnld  48452  dignn0flhalf  48467  2arymaptfo  48503  itcovalt2lem1  48524  prelrrx2  48562  eenglngeehlnmlem2  48587  rrxsphere  48597  line2  48601  line2x  48603  line2y  48604  itsclc0yqsollem2  48612  inlinecirc02plem  48635  sepfsepc  48723  alimp-surprise  49010  aacllem  49031