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  4132  ssini  4181  opthhausdorff  5465  elvv  5699  elopaelxp  5714  relopabiv  5769  relopabi  5771  dfpo2  6254  funpr  6548  funcnvpr  6554  mpov  7472  caovcom  7557  snnex  7705  pwnex  7706  1st2val  7963  2nd2val  7964  elxp7  7970  opreuopreu  7980  poxp2  8086  poseq  8101  tfr1a  8326  oeoa  8526  oeoe  8528  erov  8754  endisj  8995  snopfsupp  9297  ssttrcl  9627  ttrclselem2  9638  r1funlim  9681  dfac2b  10044  cflecard  10166  canth4  10561  canthnumlem  10562  canthwelem  10564  canthp1lem2  10567  pwfseqlem4  10576  wunex3  10655  addsrpr  10989  mulsrpr  10990  recexsrlem  11017  mulcani  11780  div1  11835  recdiv  11852  divdiv1  11857  divdiv2  11858  div23i  11904  div11i  11905  divmuldivi  11906  divadddivi  11908  divdivdivi  11909  lemulge11  12009  negiso  12127  dfnn3  12179  2cnne0  12377  2rene0  12378  halfpm6th  12390  avglt1  12406  avglt2  12407  div4p1lem1div2  12423  3halfnz  12599  divlt1lt  13004  divle1le  13005  nnledivrp  13047  x2times  13242  xrsupsslem  13250  xrinfmsslem  13251  nnge2recico01  13451  fvf1tp  13739  om2uzoi  13908  fzennn  13921  expge1  14052  sqoddm1div8  14196  faclbnd2  14244  faclbnd4lem1  14246  4bc2eq6  14282  hashfxnn0  14290  hashsnlei  14371  hashunlei  14378  hashsslei  14379  hash2prb  14425  repswccat  14739  funcnvs4  14868  f1oun2prg  14870  wrdlen2i  14895  s2rn  14916  s3rn  14917  s7rn  14918  relexpaddg  15006  cjreb  15076  sqrt2gt1lt2  15227  abs1m  15289  bpoly3  16014  ege2le3  16046  efi4p  16095  efival  16110  sin01bnd  16143  cos01bnd  16144  cos1bnd  16145  cos2bnd  16146  sin01gt0  16148  cos01gt0  16149  sin02gt0  16150  sincos2sgn  16152  sin4lt0  16153  egt2lt3  16164  rpnnen2lem3  16174  rpnnen2lem11  16182  nthruc  16210  nthruz  16211  3dvdsdec  16292  3dvds2dec  16293  mod2eq1n2dvds  16307  halfleoddlt  16322  divalglem5  16357  ndvdsi  16372  flodddiv4  16375  flodddiv4lt  16377  bitsp1o  16393  3lcm2e6woprm  16575  6lcm4e12  16576  pcrec  16820  prmrec  16884  prmgaplcmlem1  17013  prmgaplcm  17022  modsubi  17034  structfn  17117  strleun  17118  slotsdifipndx  17289  slotsdifplendx  17329  slotsdifdsndx  17348  slotsdifunifndx  17355  slotsdifplendx2  17370  slotsdifocndx  17371  isofn  17733  sscres  17781  funcestrcsetclem7  18103  funcestrcsetclem8  18104  fullestrcsetc  18108  nulchn  18576  chninf  18592  mgmnsgrpex  18893  pwmnd  18899  ga0  19264  symg2bas  19359  f1otrspeq  19413  psgnsn  19486  0frgp  19745  gsummptnn0fz  19952  srgbinomlem4  20201  isrnghm  20412  rnghmsscmap2  20597  rnghmsscmap  20598  funcrngcsetc  20608  funcrngcsetcALT  20609  rhmsscmap2  20626  rhmsscmap  20627  funcringcsetc  20642  cnfldfun  21358  cnfldfunALT  21359  cnfldfunOLD  21371  cnfldfunALTOLD  21372  cnfld1  21383  cnfld1OLD  21384  cnsubdrglem  21408  expmhm  21426  expghm  21465  pzriprnglem4  21474  pzriprnglem9  21479  pzriprnglem14  21484  pzriprng1ALT  21486  psrbag0  22050  psrbagsn  22051  coe1fsupp  22188  coe1mul2  22244  evls1sca  22298  matmulr  22413  mat1dimelbas  22446  mat1f1o  22453  m2detleib  22606  smadiadetglem1  22646  pmatcollpw3fi1lem2  22762  cpmidpmatlem2  22846  cpmadumatpolylem1  22856  cayhamlem3  22862  cayhamlem4  22863  isbasis3g  22924  fctop  22979  cctop  22981  refref  23488  bl2in  24375  dscmet  24547  iihalf1  24908  iihalf2  24910  icopnfhmeo  24920  iccpnfhmeo  24922  xrhmeo  24923  iscvsi  25106  zclmncvs  25125  ncvs1  25134  ehl2eudis  25399  minveclem2  25403  minveclem4  25409  ovolunlem1a  25473  volf  25506  i1f1lem  25666  mbfi1fseqlem5  25696  dveflem  25956  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  26780  ang180lem1  26786  1cubrlem  26818  quart1  26833  log2cnv  26921  log2tlbnd  26922  log2ublem1  26923  log2ub  26926  emcllem1  26973  emcllem6  26978  basellem1  27058  basellem2  27059  basellem3  27060  basellem8  27065  ppiublem1  27179  ppiublem2  27180  ppiub  27181  chtublem  27188  chtub  27189  bcmono  27254  bclbnd  27257  bpos1lem  27259  bposlem1  27261  bposlem2  27262  bposlem3  27263  bposlem4  27264  bposlem5  27265  bposlem6  27266  bposlem7  27267  bposlem8  27268  bposlem9  27269  lgsdir2lem1  27302  1lgs  27317  gausslemma2dlem0c  27335  gausslemma2dlem0d  27336  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  gausslemma2dlem3  27345  gausslemma2dlem5  27348  gausslemma2dlem6  27349  lgsquad2lem2  27362  2lgslem1a1  27366  2lgslem1a2  27367  2lgslem1c  27370  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  2lgslem3  27381  2lgsoddprmlem1  27385  addsqrexnreu  27419  addsqnreup  27420  chebbnd1lem1  27446  chebbnd1lem3  27448  chebbnd1  27449  dchrisum0flblem2  27486  dchrisum0lem1  27493  mulog2sumlem2  27512  selberglem2  27523  chpdifbndlem1  27530  sltssnb  27775  mulscl  28140  ltmuls  28142  divs1  28210  precsexlem8  28220  0reno  28502  1reno  28503  slotsinbpsd  28523  slotslnbpsd  28524  ercgrg  28599  axlowdimlem4  29028  axlowdimlem5  29029  axlowdimlem6  29030  axlowdimlem7  29031  axlowdimlem8  29032  axlowdimlem10  29034  axlowdimlem11  29035  graop  29112  grastruct  29113  uhgrunop  29158  upgrop  29177  upgrunop  29202  umgrunop  29204  usgrop  29246  usgr2v1e2w  29335  usgrexmpldifpr  29341  usgrexmpledg  29345  uhgrsubgrself  29363  uhgrspan1lem1  29383  upgrres1lem1  29392  fusgrfis  29413  vtxd0nedgb  29572  p1evtxdeqlem  29596  p1evtxdeq  29597  p1evtxdp1  29598  umgr2v2e  29609  vdegp1bi  29621  wlkcomp  29714  upgr2pthnlp  29815  usgr2trlncl  29843  usgr2pthlem  29846  clwlkcomp  29862  uspgrn2crct  29891  wwlksonvtx  29938  wspthnonp  29942  2wlkond  30020  2pthond  30025  2pthon3v  30026  umgr2adedgwlkonALT  30030  umgr2wlk  30032  umgr2wlkon  30033  wpthswwlks2on  30047  elwspths2spth  30053  0ewlk  30199  0pth  30210  0pthonv  30214  1pthon2v  30238  3wlkdlem4  30247  3trlond  30258  3pthond  30260  3spthond  30262  trlsegvdeglem3  30307  eupthvdres  30320  eupth2lemb  30322  ex-natded5.2i  30491  ex-an  30507  ex-id  30519  ex-po  30520  ex-fl  30532  ex-mod  30534  ex-exp  30535  ex-lcm  30543  nvz0  30754  ipidsq  30796  ipdirilem  30915  siilem1  30937  minvecolem2  30961  minvecolem3  30962  minvecolem4  30966  hvsubcan  31160  hvsubcan2  31161  normlem7tALT  31205  helch  31329  hsn0elch  31334  hhshsslem2  31354  hhsssh  31355  shscli  31403  shintcli  31415  shintcl  31416  chintcli  31417  chintcl  31418  shincli  31448  shsval2i  31473  omlsi  31490  chincli  31546  chabs1  31602  fh1i  31707  fh2i  31708  cm2ji  31711  pjnormi  31807  nmopsetn0  31951  nmfnsetn0  31964  lnophm  32105  nmcexi  32112  nmbdfnlb  32136  imaelshi  32144  nlelshi  32146  nmopadjlem  32175  nmopcoadji  32187  hmopidmch  32239  hmopidmpj  32240  sto1i  32322  stlei  32326  stji1i  32328  csmdsymi  32420  chirred  32481  cdj3lem1  32520  rpdp2cl  32956  dp2lt10  32958  dp2lt  32959  dp2ltc  32961  dpfrac1  32966  dplti  32979  dpgti  32980  dpexpp1  32982  dpadd3  32986  dpmul  32987  dpmul4  32988  xrsclat  33086  nn0archi  33422  zringfrac  33629  cos9thpiminplylem4  33945  cos9thpiminplylem5  33946  cos9thpinconstr  33951  lmatfvlem  33975  xrge0iifmhm  34099  qqh0  34144  qqh1  34145  rerrext  34169  cnrrext  34170  prsiga  34291  oms0  34457  coinfliprv  34643  ballotlem1  34647  ballotth  34698  signsw0g  34716  hgt750lemd  34808  hgt750lem  34811  hgt750lem2  34812  hgt750leme  34818  tgoldbachgt  34823  subfacval2  35385  erdszelem2  35390  cvmliftlem4  35486  satom  35554  satfv1  35561  sat1el2xp  35577  fmlaomn0  35588  satfdmfmla  35598  satfv1fvfmla1  35621  ex-sategoelelomsuc  35624  ex-sategoelel12  35625  prv0  35628  prv1n  35629  elmrsubrn  35718  msubfval  35722  problem4  35866  quad3  35868  br6  35955  dfon2lem3  35981  fullfunfnv  36144  itgeq12i  36404  fneref  36548  filnetlem2  36577  filnetlem3  36578  onpsstopbas  36628  dfttc3gw  36721  dfttc4lem2  36727  dnizeq0  36751  dnibndlem12  36765  knoppcnlem5  36773  knoppcnlem8  36776  knoppcnlem11  36779  knoppndvlem14  36801  cnndvlem1  36813  bj-genr  36888  bj-genl  36889  bj-genan  36890  bj-2upln1upl  37347  bj-vtoclgfALT  37382  bj-brab2a1  37479  bj-opabssvv  37480  taupilem1  37651  topdifinf  37679  sin2h  37945  cos2h  37946  tan2h  37947  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem26  37981  poimirlem29  37984  poimirlem31  37986  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  itg2addnclem2  38007  asindmre  38038  heiborlem7  38152  riscer  38323  refrelcoss3  38888  symrelcoss3  38890  ishlatiN  39815  0psubN  40209  atpsubN  40213  gcdcomnni  42441  gcdnegnni  42442  neggcdnni  42443  60gcd7e1  42458  lcmeprodgcdi  42460  lcm2un  42467  lcm3un  42468  lcmineqlem4  42485  lcmineqlem6  42487  3lexlogpow5ineq1  42507  aks4d1p1p2  42523  mzpclall  43173  diophin  43218  diophun  43219  eldioph4b  43257  irrapx1  43274  2nn0ind  43391  aomclem4  43503  onexlimgt  43689  nnoeomeqom  43758  oaomoencom  43763  oenassex  43764  succlg  43774  dflim5  43775  omabs2  43778  tfsconcatfv2  43786  ifpid3g  43937  ifpid2g  43938  ifpbi1b  43948  eu0  43965  pwinfi  44009  rtrclex  44062  cnvrcl0  44070  dfrcl2  44119  relexp1idm  44159  relexp0idm  44160  clsk1independent  44491  lhe4.4ex1a  44774  expgrowth  44780  ax6e2nd  45003  uun0.1  45222  relopabVD  45345  ax6e2ndVD  45352  sb5ALTVD  45357  ax6e2ndALT  45374  permaxinf2lem  45457  rexanuz2nf  45938  dvmptconst  46361  dvmptidg  46363  dvmulcncf  46371  dvdivcncf  46373  dvnprodlem3  46394  itgsinexplem1  46400  volioof  46433  stoweidlem13  46459  stoweidlem14  46460  stoweidlem26  46472  stoweidlem34  46480  stoweidlem49  46495  stoweidlem59  46505  dirkertrigeqlem3  46546  dirkercncflem1  46549  dirkercncflem2  46550  fourierdlem57  46609  fourierdlem62  46614  fourierdlem103  46655  fourierdlem111  46663  fourierswlem  46676  fouriersw  46677  salexct2  46785  salexct3  46788  salgencntex  46789  salgensscntex  46790  gsumge0cl  46817  sge00  46822  sge0tsms  46826  0ome  46975  ovnlecvr  47004  ovn0lem  47011  hoidmvle  47046  ovnsubadd2lem  47091  smflimlem6  47222  mbfpsssmf  47229  smfmullem4  47240  smfpimbor1lem1  47244  nthrucw  47332  cjnpoly  47349  sinnpoly  47351  astbstanbst  47369  aistbistaandb  47370  abnotataxb  47376  aifftbifffaibif  47381  confun4  47402  plcofph  47404  plvcofph  47406  plvcofphax  47407  plvofpos  47408  mdandyv0  47409  mdandyv1  47410  mdandyv2  47411  mdandyv3  47412  mdandyv4  47413  mdandyv5  47414  mdandyv6  47415  mdandyv7  47416  mdandyv8  47417  mdandyv9  47418  mdandyv10  47419  mdandyv11  47420  mdandyv12  47421  mdandyv13  47422  mdandyv14  47423  mdandyv15  47424  mdandyvr0  47425  mdandyvr1  47426  mdandyvr2  47427  mdandyvr3  47428  mdandyvr4  47429  mdandyvr5  47430  mdandyvr6  47431  mdandyvr7  47432  mdandyvrx0  47441  mdandyvrx1  47442  mdandyvrx2  47443  mdandyvrx3  47444  mdandyvrx4  47445  mdandyvrx5  47446  mdandyvrx6  47447  mdandyvrx7  47448  dandysum2p2e4  47458  or2expropbilem1  47492  dfnelbr2  47733  2ltceilhalf  47792  flmrecm1  47803  ich2exprop  47943  paireqne  47983  fmtno4prmfac  48047  31prm  48072  lighneallem4a  48083  41prothprmlem2  48093  ppivalnn4  48102  zofldiv2ALTV  48150  nfermltl8rev  48230  nfermltl2rev  48231  nfermltlrev  48232  gbegt5  48249  gbowgt5  48250  gboge9  48252  9gbo  48262  11gbo  48263  nnsum3primes4  48276  nnsum3primesgbe  48280  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  tgblthelfgott  48303  tgoldbach  48305  ushggricedg  48415  isubgrgrim  48417  stgrvtx  48442  stgriedg  48443  stgrusgra  48447  stgr1  48449  uspgrlim  48480  grlimprclnbgrvtx  48487  clnbgr3stgrgrlic  48508  usgrexmpl1lem  48509  usgrexmpl2lem  48514  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  gpgvtx  48531  gpgiedg  48532  gpgorder  48547  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgedgiov  48553  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg3kgrtriexlem3  48573  gpg3kgrtriexlem6  48576  gpgprismgr4cycllem2  48584  gpgprismgr4cyclex  48595  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnioedg5  48600  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5lem3  48610  pgnbgreunbgrlem6  48612  gpg5ngric  48616  gpg5edgnedg  48618  nn0mnd  48667  mgmplusgiopALT  48682  sgrp2sgrp  48716  2zrngaabl  48738  funcringcsetcALTV2lem8  48785  funcringcsetclem8ALTV  48808  zlmodzxzlmod  48842  zlmodzxzel  48843  zlmodzxzscm  48845  zlmodzxzadd  48846  snlindsntorlem  48958  ldepspr  48961  lmod1lem2  48976  lmod1lem3  48977  lmod1lem4  48978  lmod1lem5  48979  lmodn0  48983  zlmodzxznm  48985  zlmodzxzldeplem  48986  zlmodzxzldeplem1  48988  zlmodzxzldeplem3  48990  lvecpsslmod  48995  ldepsnlinc  48996  ldepslinc  48997  expnegico01  49006  zofldiv2  49019  flnn0div2ge  49021  elbigo2  49040  nnlog2ge0lt1  49054  digfval  49085  dignnld  49091  dignn0flhalf  49106  2arymaptfo  49142  itcovalt2lem1  49163  prelrrx2  49201  eenglngeehlnmlem2  49226  rrxsphere  49236  line2  49240  line2x  49242  line2y  49243  itsclc0yqsollem2  49251  inlinecirc02plem  49274  sepfsepc  49415  invfn  49517  alimp-surprise  50267  aacllem  50288