Theorem pm3.2i 471

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

Syntax hints:   ∧ wa 396

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 397

This theorem is referenced by:  mp4an  690  pm4.87  840  3pm3.2i  1338  unssi  4120  ssini  4166  opthhausdorff  5432  elvv  5662  elopaelxp  5677  relopabiv  5732  relopabi  5734  dfpo2  6203  funpr  6497  funcnvpr  6503  mpov  7395  caovcom  7478  snnex  7617  pwnex  7618  1st2val  7868  2nd2val  7869  elxp7  7875  opreuopreu  7885  mptmpoopabbrdOLD  7932  wfrlem13OLD  8161  wfr3OLD  8178  tfr1a  8234  oeoa  8437  oeoe  8439  erov  8612  endisj  8854  phplem2OLD  9010  snopfsupp  9160  ssttrcl  9482  ttrclselem2  9493  r1funlim  9533  dfac2b  9895  cflecard  10018  canth4  10412  canthnumlem  10413  canthwelem  10415  canthp1lem2  10418  pwfseqlem4  10427  wunex3  10506  addsrpr  10840  mulsrpr  10841  recexsrlem  10868  mulcani  11623  div1  11673  recdiv  11690  divdiv1  11695  divdiv2  11696  div23i  11742  div11i  11743  divmuldivi  11744  divadddivi  11746  divdivdivi  11747  lemulge11  11846  negiso  11964  dfnn3  11996  2cnne0  12192  2rene0  12193  halfpm6th  12203  avglt1  12220  avglt2  12221  div4p1lem1div2  12237  3halfnz  12408  divlt1lt  12808  divle1le  12809  nnledivrp  12851  x2times  13042  xrsupsslem  13050  xrinfmsslem  13051  fz0to4untppr  13368  om2uzoi  13684  fzennn  13697  expge1  13829  sqoddm1div8  13967  faclbnd2  14014  faclbnd4lem1  14016  4bc2eq6  14052  hashfxnn0  14060  hashsnlei  14142  hashunlei  14149  hashsslei  14150  hash2prb  14195  repswccat  14508  cshwsexa  14546  funcnvs4  14637  f1oun2prg  14639  wrdlen2i  14664  relexpaddg  14773  cjreb  14843  sqrt2gt1lt2  14995  abs1m  15056  bpoly3  15777  ege2le3  15808  efi4p  15855  efival  15870  sin01bnd  15903  cos01bnd  15904  cos1bnd  15905  cos2bnd  15906  sin01gt0  15908  cos01gt0  15909  sin02gt0  15910  sincos2sgn  15912  sin4lt0  15913  egt2lt3  15924  rpnnen2lem3  15934  rpnnen2lem11  15942  nthruc  15970  nthruz  15971  3dvdsdec  16050  3dvds2dec  16051  mod2eq1n2dvds  16065  halfleoddlt  16080  divalglem5  16115  ndvdsi  16130  flodddiv4  16131  flodddiv4lt  16133  bitsp1o  16149  3lcm2e6woprm  16329  6lcm4e12  16330  pcrec  16568  prmrec  16632  prmgaplcmlem1  16761  prmgaplcm  16770  modsubi  16782  structfn  16866  strleun  16867  slotsdifipndx  17054  slotsdifplendx  17094  slotsdifdsndx  17113  slotsdifunifndx  17120  slotsdifplendx2  17136  slotsdifocndx  17137  isofn  17496  sscres  17544  funcestrcsetclem7  17872  funcestrcsetclem8  17873  fullestrcsetc  17877  mgmnsgrpex  18579  pwmnd  18585  ga0  18913  symg2bas  19009  f1otrspeq  19064  psgnsn  19137  0frgp  19394  gsummptnn0fz  19596  srgbinomlem4  19788  cnfldfun  20618  cnfldfunALT  20619  cnfldfunALTOLD  20620  cnfld1  20632  cnsubdrglem  20658  expmhm  20676  expghm  20706  psrbag0  21279  psrbagsn  21280  coe1fsupp  21394  coe1mul2  21449  evls1sca  21498  matmulr  21596  mat1dimelbas  21629  mat1f1o  21636  m2detleib  21789  smadiadetglem1  21829  pmatcollpw3fi1lem2  21945  cpmidpmatlem2  22029  cpmadumatpolylem1  22039  cayhamlem3  22045  cayhamlem4  22046  isbasis3g  22108  fctop  22163  cctop  22165  refref  22673  bl2in  23562  dscmet  23737  iihalf1  24103  iihalf2  24105  icopnfhmeo  24115  iccpnfhmeo  24117  xrhmeo  24118  iscvsi  24301  zclmncvs  24321  ncvs1  24330  ehl2eudis  24595  minveclem2  24599  minveclem4  24605  ovolunlem1a  24669  volf  24702  i1f1lem  24862  mbfi1fseqlem5  24893  dveflem  25152  pilem2  25620  pilem3  25621  sinhalfpilem  25629  sincosq1lem  25663  tangtx  25671  sinq12gt0  25673  sincos4thpi  25679  sincos6thpi  25681  sincos3rdpi  25682  pigt3  25683  pige3ALT  25685  coseq1  25690  efeq1  25693  efif1olem4  25710  angneg  25962  ang180lem1  25968  1cubrlem  26000  quart1  26015  log2cnv  26103  log2tlbnd  26104  log2ublem1  26105  log2ub  26108  emcllem1  26154  emcllem6  26159  basellem1  26239  basellem2  26240  basellem3  26241  basellem8  26246  ppiublem1  26359  ppiublem2  26360  ppiub  26361  chtublem  26368  chtub  26369  bcmono  26434  bclbnd  26437  bpos1lem  26439  bposlem1  26441  bposlem2  26442  bposlem3  26443  bposlem4  26444  bposlem5  26445  bposlem6  26446  bposlem7  26447  bposlem8  26448  bposlem9  26449  lgsdir2lem1  26482  1lgs  26497  gausslemma2dlem0c  26515  gausslemma2dlem0d  26516  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  gausslemma2dlem3  26525  gausslemma2dlem5  26528  gausslemma2dlem6  26529  lgsquad2lem2  26542  2lgslem1a1  26546  2lgslem1a2  26547  2lgslem1c  26550  2lgslem3a  26553  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  2lgslem3  26561  2lgsoddprmlem1  26565  addsqrexnreu  26599  addsqnreup  26600  chebbnd1lem1  26626  chebbnd1lem3  26628  chebbnd1  26629  dchrisum0flblem2  26666  dchrisum0lem1  26673  mulog2sumlem2  26692  selberglem2  26703  chpdifbndlem1  26710  slotsinbpsd  26811  slotslnbpsd  26812  ercgrg  26887  axlowdimlem4  27322  axlowdimlem5  27323  axlowdimlem6  27324  axlowdimlem7  27325  axlowdimlem8  27326  axlowdimlem10  27328  axlowdimlem11  27329  graop  27408  grastruct  27409  uhgrunop  27454  upgrop  27473  upgrunop  27498  umgrunop  27500  usgrop  27542  usgr2v1e2w  27628  usgrexmpldifpr  27634  usgrexmpledg  27638  uhgrsubgrself  27656  uhgrspan1lem1  27676  upgrres1lem1  27685  fusgrfis  27706  vtxd0nedgb  27864  p1evtxdeqlem  27888  p1evtxdeq  27889  p1evtxdp1  27890  umgr2v2e  27901  vdegp1bi  27913  wlkcomp  28007  upgr2pthnlp  28109  usgr2trlncl  28137  usgr2pthlem  28140  clwlkcomp  28156  uspgrn2crct  28182  wwlksonvtx  28229  wspthnonp  28233  2wlkond  28311  2pthond  28316  2pthon3v  28317  umgr2adedgwlkonALT  28321  umgr2wlk  28323  umgr2wlkon  28324  wpthswwlks2on  28335  elwspths2spth  28341  0ewlk  28487  0pth  28498  0pthonv  28502  1pthon2v  28526  3wlkdlem4  28535  3trlond  28546  3pthond  28548  3spthond  28550  trlsegvdeglem3  28595  eupthvdres  28608  eupth2lemb  28610  ex-natded5.2i  28779  ex-an  28795  ex-id  28807  ex-po  28808  ex-fl  28820  ex-mod  28822  ex-exp  28823  ex-lcm  28831  nvz0  29039  ipidsq  29081  ipdirilem  29200  siilem1  29222  minvecolem2  29246  minvecolem3  29247  minvecolem4  29251  hvsubcan  29445  hvsubcan2  29446  normlem7tALT  29490  helch  29614  hsn0elch  29619  hhshsslem2  29639  hhsssh  29640  shscli  29688  shintcli  29700  shintcl  29701  chintcli  29702  chintcl  29703  shincli  29733  shsval2i  29758  omlsi  29775  chincli  29831  chabs1  29887  fh1i  29992  fh2i  29993  cm2ji  29996  pjnormi  30092  nmopsetn0  30236  nmfnsetn0  30249  lnophm  30390  nmcexi  30397  nmbdfnlb  30421  imaelshi  30429  nlelshi  30431  nmopadjlem  30460  nmopcoadji  30472  hmopidmch  30524  hmopidmpj  30525  sto1i  30607  stlei  30611  stji1i  30613  csmdsymi  30705  chirred  30766  cdj3lem1  30805  rpdp2cl  31165  dp2lt10  31167  dp2lt  31168  dp2ltc  31170  dpfrac1  31175  dplti  31188  dpgti  31189  dpexpp1  31191  dpadd3  31195  dpmul  31196  dpmul4  31197  xrsclat  31298  nn0archi  31556  lmatfvlem  31774  xrge0iifmhm  31898  qqh0  31943  qqh1  31944  rerrext  31968  cnrrext  31969  prsiga  32108  oms0  32273  coinfliprv  32458  ballotlem1  32462  ballotth  32513  signsw0g  32544  hgt750lemd  32637  hgt750lem  32640  hgt750lem2  32641  hgt750leme  32647  tgoldbachgt  32652  subfacval2  33158  erdszelem2  33163  cvmliftlem4  33259  satom  33327  satfv1  33334  sat1el2xp  33350  fmlaomn0  33361  satfdmfmla  33371  satfv1fvfmla1  33394  ex-sategoelelomsuc  33397  ex-sategoelel12  33398  prv0  33401  prv1n  33402  elmrsubrn  33491  msubfval  33495  problem4  33635  quad3  33637  br6  33733  dfon2lem3  33770  poxp2  33799  poseq  33811  fullfunfnv  34257  fneref  34548  filnetlem2  34577  filnetlem3  34578  onpsstopbas  34628  dnizeq0  34664  dnibndlem12  34678  knoppcnlem5  34686  knoppcnlem8  34689  knoppcnlem10  34691  knoppcnlem11  34692  knoppndvlem14  34714  cnndvlem1  34726  bj-genr  34797  bj-genl  34798  bj-genan  34799  bj-2upln1upl  35223  bj-vtoclgfALT  35239  bj-brab2a1  35329  bj-opabssvv  35330  taupilem1  35501  topdifinf  35529  sin2h  35776  cos2h  35777  tan2h  35778  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem29  35815  poimirlem31  35817  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  itg2addnclem2  35838  asindmre  35869  heiborlem7  35984  riscer  36155  refrelcoss3  36588  symrelcoss3  36590  ishlatiN  37376  0psubN  37770  atpsubN  37774  gcdcomnni  40004  gcdnegnni  40005  neggcdnni  40006  60gcd7e1  40020  lcmeprodgcdi  40022  lcm2un  40029  lcm3un  40030  lcmineqlem4  40047  lcmineqlem6  40049  3lexlogpow5ineq1  40069  aks4d1p1p2  40085  mzpclall  40556  diophin  40601  diophun  40602  eldioph4b  40640  irrapx1  40657  2nn0ind  40774  aomclem4  40889  ifpid3g  41106  ifpid2g  41107  ifpbi1b  41117  eu0  41134  pwinfi  41178  rtrclex  41232  cnvrcl0  41240  dfrcl2  41289  relexp1idm  41329  relexp0idm  41330  clsk1independent  41663  lhe4.4ex1a  41954  expgrowth  41960  ax6e2nd  42185  uun0.1  42405  relopabVD  42528  ax6e2ndVD  42535  sb5ALTVD  42540  ax6e2ndALT  42557  dvmptconst  43463  dvmptidg  43465  dvmulcncf  43473  dvdivcncf  43475  dvnprodlem3  43496  itgsinexplem1  43502  volioof  43535  stoweidlem13  43561  stoweidlem14  43562  stoweidlem26  43574  stoweidlem34  43582  stoweidlem49  43597  stoweidlem59  43607  dirkertrigeqlem3  43648  dirkercncflem1  43651  dirkercncflem2  43652  fourierdlem57  43711  fourierdlem62  43716  fourierdlem103  43757  fourierdlem111  43765  fourierswlem  43778  fouriersw  43779  salexct2  43885  salexct3  43888  salgencntex  43889  salgensscntex  43890  gsumge0cl  43916  sge00  43921  sge0tsms  43925  0ome  44074  ovnlecvr  44103  ovn0lem  44110  hoidmvle  44145  ovnsubadd2lem  44190  smflimlem6  44321  mbfpsssmf  44328  smfmullem4  44339  smfpimbor1lem1  44343  astbstanbst  44415  aistbistaandb  44416  abnotataxb  44422  aifftbifffaibif  44427  confun4  44448  plcofph  44450  plvcofph  44452  plvcofphax  44453  plvofpos  44454  mdandyv0  44455  mdandyv1  44456  mdandyv2  44457  mdandyv3  44458  mdandyv4  44459  mdandyv5  44460  mdandyv6  44461  mdandyv7  44462  mdandyv8  44463  mdandyv9  44464  mdandyv10  44465  mdandyv11  44466  mdandyv12  44467  mdandyv13  44468  mdandyv14  44469  mdandyv15  44470  mdandyvr0  44471  mdandyvr1  44472  mdandyvr2  44473  mdandyvr3  44474  mdandyvr4  44475  mdandyvr5  44476  mdandyvr6  44477  mdandyvr7  44478  mdandyvrx0  44487  mdandyvrx1  44488  mdandyvrx2  44489  mdandyvrx3  44490  mdandyvrx4  44491  mdandyvrx5  44492  mdandyvrx6  44493  mdandyvrx7  44494  dandysum2p2e4  44504  or2expropbilem1  44537  dfnelbr2  44776  ich2exprop  44934  paireqne  44974  fmtno4prmfac  45035  31prm  45060  lighneallem4a  45071  41prothprmlem2  45081  zofldiv2ALTV  45125  nfermltl8rev  45205  nfermltl2rev  45206  nfermltlrev  45207  gbegt5  45224  gbowgt5  45225  gboge9  45227  9gbo  45237  11gbo  45238  nnsum3primes4  45251  nnsum3primesgbe  45255  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  tgblthelfgott  45278  tgoldbach  45280  isomgrref  45298  ushrisomgr  45304  nn0mnd  45384  mgmplusgiopALT  45399  sgrp2sgrp  45433  isrnghm  45461  2zrngaabl  45513  rnghmsscmap2  45542  rnghmsscmap  45543  funcrngcsetc  45567  funcrngcsetcALT  45568  rhmsscmap2  45588  rhmsscmap  45589  funcringcsetc  45604  funcringcsetcALTV2lem8  45612  funcringcsetclem8ALTV  45635  zlmodzxzlmod  45701  zlmodzxzel  45702  zlmodzxzscm  45704  zlmodzxzadd  45705  snlindsntorlem  45822  ldepspr  45825  lmod1lem2  45840  lmod1lem3  45841  lmod1lem4  45842  lmod1lem5  45843  lmodn0  45847  zlmodzxznm  45849  zlmodzxzldeplem  45850  zlmodzxzldeplem1  45852  zlmodzxzldeplem3  45854  lvecpsslmod  45859  ldepsnlinc  45860  ldepslinc  45861  expnegico01  45870  zofldiv2  45888  flnn0div2ge  45890  elbigo2  45909  nnlog2ge0lt1  45923  digfval  45954  dignnld  45960  dignn0flhalf  45975  2arymaptfo  46011  itcovalt2lem1  46032  prelrrx2  46070  eenglngeehlnmlem2  46095  rrxsphere  46105  line2  46109  line2x  46111  line2y  46112  itsclc0yqsollem2  46120  inlinecirc02plem  46143  sepfsepc  46232  alimp-surprise  46495  aacllem  46516