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  4154  ssini  4203  opthhausdorff  5477  elvv  5713  elopaelxp  5728  relopabiv  5783  relopabi  5785  dfpo2  6269  funpr  6572  funcnvpr  6578  mpov  7501  caovcom  7586  snnex  7734  pwnex  7735  1st2val  7996  2nd2val  7997  elxp7  8003  opreuopreu  8013  mptmpoopabbrdOLDOLD  8062  poxp2  8122  poseq  8137  tfr1a  8362  oeoa  8561  oeoe  8563  erov  8787  endisj  9028  snopfsupp  9342  ssttrcl  9668  ttrclselem2  9679  r1funlim  9719  dfac2b  10084  cflecard  10206  canth4  10600  canthnumlem  10601  canthwelem  10603  canthp1lem2  10606  pwfseqlem4  10615  wunex3  10694  addsrpr  11028  mulsrpr  11029  recexsrlem  11056  mulcani  11817  div1  11872  recdiv  11888  divdiv1  11893  divdiv2  11894  div23i  11940  div11i  11941  divmuldivi  11942  divadddivi  11944  divdivdivi  11945  lemulge11  12045  negiso  12163  dfnn3  12200  2cnne0  12391  2rene0  12392  halfpm6th  12404  avglt1  12420  avglt2  12421  div4p1lem1div2  12437  3halfnz  12613  divlt1lt  13022  divle1le  13023  nnledivrp  13065  x2times  13259  xrsupsslem  13267  xrinfmsslem  13268  fvf1tp  13751  om2uzoi  13920  fzennn  13933  expge1  14064  sqoddm1div8  14208  faclbnd2  14256  faclbnd4lem1  14258  4bc2eq6  14294  hashfxnn0  14302  hashsnlei  14383  hashunlei  14390  hashsslei  14391  hash2prb  14437  repswccat  14751  cshwsexaOLD  14790  funcnvs4  14881  f1oun2prg  14883  wrdlen2i  14908  s2rn  14929  s3rn  14930  s7rn  14931  relexpaddg  15019  cjreb  15089  sqrt2gt1lt2  15240  abs1m  15302  bpoly3  16024  ege2le3  16056  efi4p  16105  efival  16120  sin01bnd  16153  cos01bnd  16154  cos1bnd  16155  cos2bnd  16156  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  sincos2sgn  16162  sin4lt0  16163  egt2lt3  16174  rpnnen2lem3  16184  rpnnen2lem11  16192  nthruc  16220  nthruz  16221  3dvdsdec  16302  3dvds2dec  16303  mod2eq1n2dvds  16317  halfleoddlt  16332  divalglem5  16367  ndvdsi  16382  flodddiv4  16385  flodddiv4lt  16387  bitsp1o  16403  3lcm2e6woprm  16585  6lcm4e12  16586  pcrec  16829  prmrec  16893  prmgaplcmlem1  17022  prmgaplcm  17031  modsubi  17043  structfn  17126  strleun  17127  slotsdifipndx  17298  slotsdifplendx  17338  slotsdifdsndx  17357  slotsdifunifndx  17364  slotsdifplendx2  17379  slotsdifocndx  17380  isofn  17737  sscres  17785  funcestrcsetclem7  18107  funcestrcsetclem8  18108  fullestrcsetc  18112  mgmnsgrpex  18858  pwmnd  18864  ga0  19230  symg2bas  19323  f1otrspeq  19377  psgnsn  19450  0frgp  19709  gsummptnn0fz  19916  srgbinomlem4  20138  isrnghm  20350  rnghmsscmap2  20538  rnghmsscmap  20539  funcrngcsetc  20549  funcrngcsetcALT  20550  rhmsscmap2  20567  rhmsscmap  20568  funcringcsetc  20583  cnfldfun  21278  cnfldfunALT  21279  cnfldfunOLD  21291  cnfldfunALTOLD  21292  cnfld1  21305  cnfld1OLD  21306  cnsubdrglem  21335  expmhm  21353  expghm  21385  pzriprnglem4  21394  pzriprnglem9  21399  pzriprnglem14  21404  pzriprng1ALT  21406  psrbag0  21969  psrbagsn  21970  coe1fsupp  22099  coe1mul2  22155  evls1sca  22210  matmulr  22325  mat1dimelbas  22358  mat1f1o  22365  m2detleib  22518  smadiadetglem1  22558  pmatcollpw3fi1lem2  22674  cpmidpmatlem2  22758  cpmadumatpolylem1  22768  cayhamlem3  22774  cayhamlem4  22775  isbasis3g  22836  fctop  22891  cctop  22893  refref  23400  bl2in  24288  dscmet  24460  iihalf1  24825  iihalf2  24828  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  iscvsi  25029  zclmncvs  25048  ncvs1  25057  ehl2eudis  25322  minveclem2  25326  minveclem4  25332  ovolunlem1a  25397  volf  25430  i1f1lem  25590  mbfi1fseqlem5  25620  dveflem  25883  pilem2  26362  pilem3  26363  sinhalfpilem  26372  sincosq1lem  26406  tangtx  26414  sinq12gt0  26416  sincos4thpi  26422  sincos6thpi  26425  sincos3rdpi  26426  pigt3  26427  pige3ALT  26429  coseq1  26434  efeq1  26437  efif1olem4  26454  angneg  26713  ang180lem1  26719  1cubrlem  26751  quart1  26766  log2cnv  26854  log2tlbnd  26855  log2ublem1  26856  log2ub  26859  emcllem1  26906  emcllem6  26911  basellem1  26991  basellem2  26992  basellem3  26993  basellem8  26998  ppiublem1  27113  ppiublem2  27114  ppiub  27115  chtublem  27122  chtub  27123  bcmono  27188  bclbnd  27191  bpos1lem  27193  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem7  27201  bposlem8  27202  bposlem9  27203  lgsdir2lem1  27236  1lgs  27251  gausslemma2dlem0c  27269  gausslemma2dlem0d  27270  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem3  27279  gausslemma2dlem5  27282  gausslemma2dlem6  27283  lgsquad2lem2  27296  2lgslem1a1  27300  2lgslem1a2  27301  2lgslem1c  27304  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgslem3  27315  2lgsoddprmlem1  27319  addsqrexnreu  27353  addsqnreup  27354  chebbnd1lem1  27380  chebbnd1lem3  27382  chebbnd1  27383  dchrisum0flblem2  27420  dchrisum0lem1  27427  mulog2sumlem2  27446  selberglem2  27457  chpdifbndlem1  27464  mulscl  28037  sltmul  28039  divs1  28107  precsexlem8  28116  0reno  28348  slotsinbpsd  28368  slotslnbpsd  28369  ercgrg  28444  axlowdimlem4  28872  axlowdimlem5  28873  axlowdimlem6  28874  axlowdimlem7  28875  axlowdimlem8  28876  axlowdimlem10  28878  axlowdimlem11  28879  graop  28956  grastruct  28957  uhgrunop  29002  upgrop  29021  upgrunop  29046  umgrunop  29048  usgrop  29090  usgr2v1e2w  29179  usgrexmpldifpr  29185  usgrexmpledg  29189  uhgrsubgrself  29207  uhgrspan1lem1  29227  upgrres1lem1  29236  fusgrfis  29257  vtxd0nedgb  29416  p1evtxdeqlem  29440  p1evtxdeq  29441  p1evtxdp1  29442  umgr2v2e  29453  vdegp1bi  29465  wlkcomp  29559  upgr2pthnlp  29662  usgr2trlncl  29690  usgr2pthlem  29693  clwlkcomp  29709  uspgrn2crct  29738  wwlksonvtx  29785  wspthnonp  29789  2wlkond  29867  2pthond  29872  2pthon3v  29873  umgr2adedgwlkonALT  29877  umgr2wlk  29879  umgr2wlkon  29880  wpthswwlks2on  29891  elwspths2spth  29897  0ewlk  30043  0pth  30054  0pthonv  30058  1pthon2v  30082  3wlkdlem4  30091  3trlond  30102  3pthond  30104  3spthond  30106  trlsegvdeglem3  30151  eupthvdres  30164  eupth2lemb  30166  ex-natded5.2i  30335  ex-an  30351  ex-id  30363  ex-po  30364  ex-fl  30376  ex-mod  30378  ex-exp  30379  ex-lcm  30387  nvz0  30597  ipidsq  30639  ipdirilem  30758  siilem1  30780  minvecolem2  30804  minvecolem3  30805  minvecolem4  30809  hvsubcan  31003  hvsubcan2  31004  normlem7tALT  31048  helch  31172  hsn0elch  31177  hhshsslem2  31197  hhsssh  31198  shscli  31246  shintcli  31258  shintcl  31259  chintcli  31260  chintcl  31261  shincli  31291  shsval2i  31316  omlsi  31333  chincli  31389  chabs1  31445  fh1i  31550  fh2i  31551  cm2ji  31554  pjnormi  31650  nmopsetn0  31794  nmfnsetn0  31807  lnophm  31948  nmcexi  31955  nmbdfnlb  31979  imaelshi  31987  nlelshi  31989  nmopadjlem  32018  nmopcoadji  32030  hmopidmch  32082  hmopidmpj  32083  sto1i  32165  stlei  32169  stji1i  32171  csmdsymi  32263  chirred  32324  cdj3lem1  32363  rpdp2cl  32802  dp2lt10  32804  dp2lt  32805  dp2ltc  32807  dpfrac1  32812  dplti  32825  dpgti  32826  dpexpp1  32828  dpadd3  32832  dpmul  32833  dpmul4  32834  xrsclat  32949  nn0archi  33318  zringfrac  33525  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  cos9thpinconstr  33781  lmatfvlem  33805  xrge0iifmhm  33929  qqh0  33974  qqh1  33975  rerrext  33999  cnrrext  34000  prsiga  34121  oms0  34288  coinfliprv  34474  ballotlem1  34478  ballotth  34529  signsw0g  34547  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  tgoldbachgt  34654  subfacval2  35174  erdszelem2  35179  cvmliftlem4  35275  satom  35343  satfv1  35350  sat1el2xp  35366  fmlaomn0  35377  satfdmfmla  35387  satfv1fvfmla1  35410  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  prv0  35417  prv1n  35418  elmrsubrn  35507  msubfval  35511  problem4  35655  quad3  35657  br6  35744  dfon2lem3  35773  fullfunfnv  35934  itgeq12i  36194  fneref  36338  filnetlem2  36367  filnetlem3  36368  onpsstopbas  36418  dnizeq0  36463  dnibndlem12  36477  knoppcnlem5  36485  knoppcnlem8  36488  knoppcnlem11  36491  knoppndvlem14  36513  cnndvlem1  36525  bj-genr  36594  bj-genl  36595  bj-genan  36596  bj-2upln1upl  37012  bj-vtoclgfALT  37047  bj-brab2a1  37137  bj-opabssvv  37138  taupilem1  37309  topdifinf  37337  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem29  37643  poimirlem31  37645  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnclem2  37666  asindmre  37697  heiborlem7  37811  riscer  37982  refrelcoss3  38454  symrelcoss3  38456  ishlatiN  39348  0psubN  39743  atpsubN  39747  gcdcomnni  41976  gcdnegnni  41977  neggcdnni  41978  60gcd7e1  41993  lcmeprodgcdi  41995  lcm2un  42002  lcm3un  42003  lcmineqlem4  42020  lcmineqlem6  42022  3lexlogpow5ineq1  42042  aks4d1p1p2  42058  mzpclall  42715  diophin  42760  diophun  42761  eldioph4b  42799  irrapx1  42816  2nn0ind  42934  aomclem4  43046  onexlimgt  43232  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  44318  expgrowth  44324  ax6e2nd  44548  uun0.1  44767  relopabVD  44890  ax6e2ndVD  44897  sb5ALTVD  44902  ax6e2ndALT  44919  permaxinf2lem  45002  rexanuz2nf  45488  dvmptconst  45913  dvmptidg  45915  dvmulcncf  45923  dvdivcncf  45925  dvnprodlem3  45946  itgsinexplem1  45952  volioof  45985  stoweidlem13  46011  stoweidlem14  46012  stoweidlem26  46024  stoweidlem34  46032  stoweidlem49  46047  stoweidlem59  46057  dirkertrigeqlem3  46098  dirkercncflem1  46101  dirkercncflem2  46102  fourierdlem57  46161  fourierdlem62  46166  fourierdlem103  46207  fourierdlem111  46215  fourierswlem  46228  fouriersw  46229  salexct2  46337  salexct3  46340  salgencntex  46341  salgensscntex  46342  gsumge0cl  46369  sge00  46374  sge0tsms  46378  0ome  46527  ovnlecvr  46556  ovn0lem  46563  hoidmvle  46598  ovnsubadd2lem  46643  smflimlem6  46774  mbfpsssmf  46781  smfmullem4  46792  smfpimbor1lem1  46796  cjnpoly  46890  sinnpoly  46892  astbstanbst  46910  aistbistaandb  46911  abnotataxb  46917  aifftbifffaibif  46922  confun4  46943  plcofph  46945  plvcofph  46947  plvcofphax  46948  plvofpos  46949  mdandyv0  46950  mdandyv1  46951  mdandyv2  46952  mdandyv3  46953  mdandyv4  46954  mdandyv5  46955  mdandyv6  46956  mdandyv7  46957  mdandyv8  46958  mdandyv9  46959  mdandyv10  46960  mdandyv11  46961  mdandyv12  46962  mdandyv13  46963  mdandyv14  46964  mdandyv15  46965  mdandyvr0  46966  mdandyvr1  46967  mdandyvr2  46968  mdandyvr3  46969  mdandyvr4  46970  mdandyvr5  46971  mdandyvr6  46972  mdandyvr7  46973  mdandyvrx0  46982  mdandyvrx1  46983  mdandyvrx2  46984  mdandyvrx3  46985  mdandyvrx4  46986  mdandyvrx5  46987  mdandyvrx6  46988  mdandyvrx7  46989  dandysum2p2e4  46999  or2expropbilem1  47033  dfnelbr2  47274  2ltceilhalf  47329  ich2exprop  47472  paireqne  47512  fmtno4prmfac  47573  31prm  47598  lighneallem4a  47609  41prothprmlem2  47619  zofldiv2ALTV  47663  nfermltl8rev  47743  nfermltl2rev  47744  nfermltlrev  47745  gbegt5  47762  gbowgt5  47763  gboge9  47765  9gbo  47775  11gbo  47776  nnsum3primes4  47789  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  tgblthelfgott  47816  tgoldbach  47818  ushggricedg  47927  isubgrgrim  47929  stgrvtx  47953  stgriedg  47954  stgrusgra  47958  stgr1  47960  uspgrlim  47991  clnbgr3stgrgrlic  48011  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  gpgvtx  48034  gpgiedg  48035  gpgorder  48050  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedgiov  48056  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem6  48079  gpgprismgr4cycllem2  48086  gpgprismgr4cyclex  48097  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgrlem6  48114  gpg5ngric  48118  nn0mnd  48167  mgmplusgiopALT  48182  sgrp2sgrp  48216  2zrngaabl  48238  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  zlmodzxzlmod  48342  zlmodzxzel  48343  zlmodzxzscm  48345  zlmodzxzadd  48346  snlindsntorlem  48459  ldepspr  48462  lmod1lem2  48477  lmod1lem3  48478  lmod1lem4  48479  lmod1lem5  48480  lmodn0  48484  zlmodzxznm  48486  zlmodzxzldeplem  48487  zlmodzxzldeplem1  48489  zlmodzxzldeplem3  48491  lvecpsslmod  48496  ldepsnlinc  48497  ldepslinc  48498  expnegico01  48507  zofldiv2  48520  flnn0div2ge  48522  elbigo2  48541  nnlog2ge0lt1  48555  digfval  48586  dignnld  48592  dignn0flhalf  48607  2arymaptfo  48643  itcovalt2lem1  48664  prelrrx2  48702  eenglngeehlnmlem2  48727  rrxsphere  48737  line2  48741  line2x  48743  line2y  48744  itsclc0yqsollem2  48752  inlinecirc02plem  48775  sepfsepc  48916  invfn  49019  alimp-surprise  49769  aacllem  49790