Theorem pm3.2i 476

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

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mp4an  706  pm4.87  857  3pm3.2i  1358  ssini  4136  unssi  4189  opthhausdorff  5489  elvv  5725  elopaelxp  5740  relopabiv  5797  relopabi  5799  dfpo2  6299  funpr  6597  funcnvpr  6603  mpov  7533  caovcom  7619  snnex  7773  pwnex  7774  1st2val  8030  2nd2val  8031  elxp7  8037  opreuopreu  8047  poxp2  8163  poseq  8178  tfr1a  8406  oeoa  8610  oeoe  8612  erov  8839  endisj  9087  snopfsupp  9387  ssttrcl  9720  ttrclselem2  9731  r1funlimOLD  9774  dfac2b  10213  cflecard  10334  canth4  10736  canthnumlem  10737  canthwelem  10739  canthp1lem2  10742  pwfseqlem4  10751  wunex3  10830  addsrpr  11164  mulsrpr  11165  recexsrlem  11192  mulcani  11959  div1  12010  recdiv  12027  divdiv1  12032  divdiv2  12033  div23i  12079  div11i  12080  divmuldivi  12081  divadddivi  12083  divdivdivi  12084  lemulge11  12183  negiso  12301  dfnn3  12353  2cnne0  12559  2rene0  12560  halfpm6th  12572  avglt1  12588  avglt2  12589  div4p1lem1div2  12605  3halfnz  12782  divlt1lt  13195  divle1le  13196  nnledivrp  13238  x2times  13433  xrsupsslem  13441  xrinfmsslem  13442  nnge2recico01  13642  fvf1tp  13933  om2uzoi  14102  fzennn  14115  expge1  14246  sqoddm1div8  14391  faclbnd2  14439  faclbnd4lem1  14441  4bc2eq6  14477  hashfxnn0  14485  hashsnlei  14567  hashunlei  14574  hashsslei  14575  hash2prb  14621  repswccat  14942  funcnvs4  15072  f1oun2prg  15074  wrdlen2i  15099  s2rn  15122  s3rn  15123  s7rn  15124  relexpaddg  15212  cjreb  15296  sqrt2gt1lt2  15447  abs1m  15509  bpoly3  16230  ege2le3  16262  efi4p  16311  efival  16326  sin01bnd  16359  cos01bnd  16360  cos1bnd  16361  cos2bnd  16362  sin01gt0  16364  cos01gt0  16365  sin02gt0  16366  sincos2sgn  16368  sin4lt0  16369  egt2lt3  16380  rpnnen2lem3  16390  rpnnen2lem11  16398  nthruc  16426  nthruz  16427  3dvdsdec  16508  3dvds2dec  16509  mod2eq1n2dvds  16523  halfleoddlt  16538  divalglem5  16573  ndvdsi  16588  flodddiv4  16591  flodddiv4lt  16593  bitsp1o  16609  3lcm2e6woprm  16796  6lcm4e12  16797  pcrec  17042  prmrec  17106  prmgaplcmlem1  17235  prmgaplcm  17244  modsubi  17256  structfn  17340  strleun  17341  slotsdifipndx  17512  slotsdifplendx  17552  slotsdifdsndx  17571  slotsdifunifndx  17578  slotsdifplendx2  17593  slotsdifocndx  17594  isofn  17956  sscres  18004  funcestrcsetclem7  18326  funcestrcsetclem8  18327  fullestrcsetc  18331  nulchn  18799  chninf  18815  mgmnsgrpex  19136  degenmgm  19143  degenmgm2nfun  19145  degenmgm2  19146  pwmnd  19149  ga0  19518  symg2bas  19613  f1otrspeq  19667  psgnsn  19740  0frgp  19999  gsummptnn0fz  20206  srgbinomlem4  20461  isrnghm  20677  rnghmsscmap2  20887  rnghmsscmap  20888  funcrngcsetc  20898  funcrngcsetcALT  20899  rhmsscmap2  20916  rhmsscmap  20917  funcringcsetc  20932  cnfldfun  21698  cnfldfunALT  21699  cnfld1  21709  cnsubdrglem  21730  expmhm  21748  expghm  21787  pzriprnglem4  21796  pzriprnglem9  21801  pzriprnglem14  21806  pzriprng1ALT  21808  psrbag0  22377  psrbagsn  22378  coe1fsupp  22538  coe1mul2  22594  evls1sca  22647  matmulr  22759  mat1dimelbas  22792  mat1f1o  22799  m2detleib  22952  smadiadetglem1  22992  pmatcollpw3fi1lem2  23111  cpmidpmatlem2  23195  cpmadumatpolylem1  23205  cayhamlem3  23211  cayhamlem4  23212  isbasis3g  23273  fctop  23328  cctop  23330  refref  23838  bl2in  24725  dscmet  24897  iihalf1  25258  iihalf2  25260  icopnfhmeo  25270  iccpnfhmeo  25272  xrhmeo  25273  iscvsi  25456  zclmncvs  25475  ncvs1  25484  ehl2eudis  25749  minveclem2  25753  minveclem4  25759  ovolunlem1a  25823  volf  25856  i1f1lem  26016  mbfi1fseqlem5  26046  dveflem  26305  pilem2  26785  pilem3  26786  sinhalfpilem  26798  sincosq1lem  26832  tangtx  26840  sinq12gt0  26842  sincos4thpi  26848  sincos6thpi  26850  sincos3rdpi  26851  pigt3  26852  pige3ALT  26854  coseq1  26859  efeq1  26862  efif1olem4  26879  angneg  27137  ang180lem1  27143  1cubrlem  27175  quart1  27190  log2cnv  27278  log2tlbnd  27279  log2ublem1  27280  log2ub  27283  emcllem1  27329  emcllem6  27334  basellem1  27414  basellem2  27415  basellem3  27416  basellem8  27421  ppiublem1  27535  ppiublem2  27536  ppiub  27537  chtublem  27544  chtub  27545  bcmono  27610  bclbnd  27613  bpos1lem  27615  bposlem1  27617  bposlem2  27618  bposlem3  27619  bposlem4  27620  bposlem5  27621  bposlem6  27622  bposlem7  27623  bposlem8  27624  bposlem9  27625  lgsdir2lem1  27658  1lgs  27673  gausslemma2dlem0c  27691  gausslemma2dlem0d  27692  gausslemma2dlem1a  27698  gausslemma2dlem2  27700  gausslemma2dlem3  27701  gausslemma2dlem5  27704  gausslemma2dlem6  27705  lgsquad2lem2  27718  2lgslem1a1  27722  2lgslem1a2  27723  2lgslem1c  27726  2lgslem3a  27729  2lgslem3b  27730  2lgslem3c  27731  2lgslem3d  27732  2lgslem3  27737  2lgsoddprmlem1  27741  addsqrexnreu  27775  addsqnreup  27776  chebbnd1lem1  27802  chebbnd1lem3  27804  chebbnd1  27805  dchrisum0flblem2  27842  dchrisum0lem1  27849  mulog2sumlem2  27868  selberglem2  27879  chpdifbndlem1  27886  sltssnb  28161  mulscl  28526  ltmuls  28528  divs1  28596  precsexlem8  28606  0reno  28888  1reno  28889  slotsinbpsd  28909  slotslnbpsd  28910  ercgrg  28986  axlowdimlem4  29529  axlowdimlem5  29530  axlowdimlem6  29531  axlowdimlem7  29532  axlowdimlem8  29533  axlowdimlem10  29535  axlowdimlem11  29536  graop  29613  grastruct  29614  uhgrunop  29659  upgrop  29678  upgrunop  29703  umgrunop  29705  usgrop  29750  usgr2v1e2w  29839  usgrexmpldifpr  29845  usgrexmpledg  29849  uhgrsubgrself  29867  uhgrspan1lem1  29887  upgrres1lem1  29896  fusgrfis  29917  vtxd0nedgb  30075  p1evtxdeqlem  30099  p1evtxdeq  30100  p1evtxdp1  30101  umgr2v2e  30112  vdegp1bi  30124  wlkcomp  30217  upgr2pthnlp  30324  usgr2trlncl  30352  usgr2pthlem  30355  clwlkcomp  30372  uspgrn2crct  30403  wwlksonvtx  30450  wspthnonp  30454  2wlkond  30532  2pthond  30537  2pthon3v  30538  umgr2adedgwlkonALT  30542  umgr2wlk  30544  umgr2wlkon  30545  wpthswwlks2on  30559  elwspths2spth  30565  0ewlk  30711  0pth  30722  0pthonv  30726  1pthon2v  30760  3wlkdlem4  30769  3trlond  30780  3pthond  30782  3spthond  30784  trlsegvdeglem3  30829  eupthvdres  30842  eupth2lemb  30844  ex-natded5.2i  31013  ex-an  31029  ex-id  31041  ex-po  31042  ex-fl  31054  ex-mod  31056  ex-exp  31057  ex-lcm  31065  nvz0  31276  ipidsq  31318  ipdirilem  31437  siilem1  31459  minvecolem2  31483  minvecolem3  31484  minvecolem4  31488  hvsubcan  31682  hvsubcan2  31683  normlem7tALT  31727  helch  31851  hsn0elch  31856  hhshsslem2  31876  hhsssh  31877  shscli  31925  shintcli  31937  shintcl  31938  chintcli  31939  chintcl  31940  shincli  31970  shsval2i  31995  omlsi  32012  chincli  32068  chabs1  32124  fh1i  32229  fh2i  32230  cm2ji  32233  pjnormi  32329  nmopsetn0  32473  nmfnsetn0  32486  lnophm  32627  nmcexi  32634  nmbdfnlb  32658  imaelshi  32666  nlelshi  32668  nmopadjlem  32697  nmopcoadji  32709  hmopidmch  32761  hmopidmpj  32762  sto1i  32844  stlei  32848  stji1i  32850  csmdsymi  32942  chirred  33003  cdj3lem1  33042  rpdp2cl  33495  dp2lt10  33497  dp2lt  33498  dp2ltc  33500  dpfrac1  33505  dplti  33518  dpgti  33519  dpexpp1  33521  dpadd3  33525  dpmul  33526  dpmul4  33527  xrsclat  33619  nn0archi  33955  zringfrac  34133  cos9thpiminplylem4  34464  cos9thpiminplylem5  34465  cos9thpinconstr  34470  lmatfvlem  34494  xrge0iifmhm  34618  qqh0  34663  qqh1  34664  rerrext  34688  cnrrext  34689  prsiga  34810  oms0  34976  coinfliprv  35162  ballotlem1  35166  ballotth  35217  signsw0g  35232  hgt750lemd  35324  hgt750lem  35327  hgt750lem2  35328  hgt750leme  35334  tgoldbachgt  35339  subfacval2  36039  erdszelem2  36044  cvmliftlem4  36140  satom  36208  satfv1  36215  sat1el2xp  36231  fmlaomn0  36242  satfdmfmla  36252  satfv1fvfmla1  36275  ex-sategoelelomsuc  36278  ex-sategoelel12  36279  prv0  36282  prv1n  36283  elmrsubrn  36372  msubfval  36376  problem4  36520  quad3  36522  br6  36615  dfon2lem3  36640  fullfunfnv  36803  itgeq12i  37088  fneref  37231  filnetlem2  37260  filnetlem3  37261  onpsstopbas  37311  dfttc3gw  37404  dfttc4lem2  37410  dnizeq0  37434  dnibndlem12  37448  knoppcnlem5  37456  knoppcnlem8  37459  knoppcnlem11  37462  knoppndvlem14  37484  cnndvlem1  37496  bj-genr  37570  bj-genl  37571  bj-genan  37572  bj-2upln1upl  38030  coi1in  38054  bj-vtoclgfALT  38067  bj-brab2a1  38164  bj-opabssvv  38165  taupilem1  38336  qdiff  38342  topdifinf  38366  sin2h  38627  cos2h  38628  tan2h  38629  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem6  38638  poimirlem7  38639  poimirlem11  38643  poimirlem12  38644  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem26  38658  poimirlem29  38661  poimirlem31  38663  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  itg2addnclem2  38684  asindmre  38715  heiborlem7  38845  riscer  39016  refrelcoss3  39579  symrelcoss3  39581  ishlatiN  40506  0psubN  40900  atpsubN  40904  gcdcomnni  43132  gcdnegnni  43133  neggcdnni  43134  60gcd7e1  43149  lcmeprodgcdi  43151  lcm2un  43158  lcm3un  43159  lcmineqlem4  43176  lcmineqlem6  43178  3lexlogpow5ineq1  43198  aks4d1p1p2  43214  25or6to4  43350  mzpclall  43832  diophin  43877  diophun  43878  eldioph4b  43912  irrapx1  43929  2nn0ind  44046  aomclem4  44153  onexlimgt  44339  nnoeomeqom  44408  oaomoencom  44413  oenassex  44414  succlg  44424  dflim5  44425  omabs2  44428  tfsconcatfv2  44436  ifpid3g  44587  ifpid2g  44588  ifpbi1b  44598  eu0  44615  pwinfi  44659  rtrclex  44711  cnvrcl0  44719  dfrcl2  44768  relexp1idm  44808  relexp0idm  44809  clsk1independent  45140  lhe4.4ex1a  45407  expgrowth  45413  ax6e2nd  45635  uun0.1  45854  relopabVD  45977  ax6e2ndVD  45984  sb5ALTVD  45989  ax6e2ndALT  46006  permaxinf2lem  46096  rexanuz2nf  46596  dvmptconst  47019  dvmptidg  47021  dvmulcncf  47029  dvdivcncf  47031  dvnprodlem3  47052  itgsinexplem1  47058  volioof  47091  stoweidlem13  47117  stoweidlem14  47118  stoweidlem26  47130  stoweidlem34  47138  stoweidlem49  47153  stoweidlem59  47163  dirkertrigeqlem3  47204  dirkercncflem1  47207  dirkercncflem2  47208  fourierdlem57  47267  fourierdlem62  47272  fourierdlem103  47313  fourierdlem111  47321  fourierswlem  47334  fouriersw  47335  salexct2  47443  salexct3  47446  salgencntex  47447  salgensscntex  47448  gsumge0cl  47475  sge00  47480  sge0tsms  47484  0ome  47633  ovnlecvr  47662  ovn0lem  47669  hoidmvle  47704  ovnsubadd2lem  47749  smflimlem6  47880  mbfpsssmf  47887  smfmullem4  47898  smfpimbor1lem1  47902  sqrtnzqaa  48008  numtowerdt  48010  goldratmolem2  48027  sqrtnpoly  48037  astbstanbst  48073  aistbistaandb  48074  abnotataxb  48080  aifftbifffaibif  48085  confun4  48106  plcofph  48108  plvcofph  48110  plvcofphax  48111  plvofpos  48112  mdandyv0  48113  mdandyv1  48114  mdandyv2  48115  mdandyv3  48116  mdandyv4  48117  mdandyv5  48118  mdandyv6  48119  mdandyv7  48120  mdandyv8  48121  mdandyv9  48122  mdandyv10  48123  mdandyv11  48124  mdandyv12  48125  mdandyv13  48126  mdandyv14  48127  mdandyv15  48128  mdandyvr0  48129  mdandyvr1  48130  mdandyvr2  48131  mdandyvr3  48132  mdandyvr4  48133  mdandyvr5  48134  mdandyvr6  48135  mdandyvr7  48136  mdandyvrx0  48145  mdandyvrx1  48146  mdandyvrx2  48147  mdandyvrx3  48148  mdandyvrx4  48149  mdandyvrx5  48150  mdandyvrx6  48151  mdandyvrx7  48152  dandysum2p2e4  48162  or2expropbilem1  48196  dfnelbr2  48437  2ltceilhalf  48496  flmrecm1  48507  ich2exprop  48647  paireqne  48687  fmtno4prmfac  48751  31prm  48776  lighneallem4a  48787  41prothprmlem2  48797  ppivalnn4  48806  zofldiv2ALTV  48854  nfermltl8rev  48934  nfermltl2rev  48935  nfermltlrev  48936  gbegt5  48953  gbowgt5  48954  gboge9  48956  9gbo  48966  11gbo  48967  nnsum3primes4  48980  nnsum3primesgbe  48984  nnsum4primesodd  48988  nnsum4primesoddALTV  48989  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  tgblthelfgott  49007  tgoldbach  49009  ushggricedg  49119  isubgrgrim  49121  stgrvtx  49146  stgriedg  49147  stgrusgra  49151  stgr1  49153  uspgrlim  49184  grlimprclnbgrvtx  49191  clnbgr3stgrgrlic  49212  usgrexmpl1lem  49213  usgrexmpl2lem  49218  usgrexmpl2nb0  49223  usgrexmpl2nb1  49224  usgrexmpl2nb2  49225  usgrexmpl2nb3  49226  usgrexmpl2nb4  49227  usgrexmpl2nb5  49228  gpgvtx  49235  gpgiedg  49236  gpgorder  49251  gpgvtxedg0  49255  gpgvtxedg1  49256  gpgedgiov  49257  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem2  49261  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem2  49264  gpg5nbgrvtx13starlem3  49265  gpg3kgrtriexlem3  49277  gpg3kgrtriexlem6  49280  gpgprismgr4cycllem2  49288  gpgprismgr4cyclex  49299  pgnioedg1  49300  pgnioedg2  49301  pgnioedg3  49302  pgnioedg4  49303  pgnioedg5  49304  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5lem1  49312  pgnbgreunbgrlem5lem2  49313  pgnbgreunbgrlem5lem3  49314  pgnbgreunbgrlem6  49316  gpg5ngric  49320  gpg5edgnedg  49322  nn0mnd  49370  mgmplusgiopALT  49385  sgrp2sgrp  49419  2zrngaabl  49441  funcringcsetcALTV2lem8  49488  funcringcsetclem8ALTV  49511  zlmodzxzlmod  49560  zlmodzxzel  49561  zlmodzxzscm  49563  zlmodzxzadd  49564  snlindsntorlem  49676  ldepspr  49679  lmod1lem2  49694  lmod1lem3  49695  lmod1lem4  49696  lmod1lem5  49697  lmodn0  49701  zlmodzxznm  49703  zlmodzxzldeplem  49704  zlmodzxzldeplem1  49706  zlmodzxzldeplem3  49708  lvecpsslmod  49713  ldepsnlinc  49714  ldepslinc  49715  expnegico01  49724  zofldiv2  49737  flnn0div2ge  49739  elbigo2  49758  nnlog2ge0lt1  49772  digfval  49803  dignnld  49809  dignn0flhalf  49824  2arymaptfo  49860  itcovalt2lem1  49881  eenglngeehlnmlem2  49945  rrxsphere  49954  line2  49958  line2x  49960  line2y  49961  itsclc0yqsollem2  49969  sepfsepc  50136  invfn  50238  par2hom  50873  fuconuniqvalslem  50877  alimp-surprise  51045  aacllem  51108