Theorem pm3.2i 472

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

Syntax hints:   ∧ wa 397

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 398

This theorem is referenced by:  mp4an  692  pm4.87  842  3pm3.2i  1340  unssi  4186  ssini  4232  opthhausdorff  5518  elvv  5751  elopaelxp  5766  relopabiv  5821  relopabi  5823  dfpo2  6296  funpr  6605  funcnvpr  6611  mpov  7520  caovcom  7604  snnex  7745  pwnex  7746  1st2val  8003  2nd2val  8004  elxp7  8010  opreuopreu  8020  mptmpoopabbrdOLD  8069  poxp2  8129  poseq  8144  wfrlem13OLD  8321  wfr3OLD  8338  tfr1a  8394  oeoa  8597  oeoe  8599  erov  8808  endisj  9058  phplem2OLD  9218  snopfsupp  9386  ssttrcl  9710  ttrclselem2  9721  r1funlim  9761  dfac2b  10125  cflecard  10248  canth4  10642  canthnumlem  10643  canthwelem  10645  canthp1lem2  10648  pwfseqlem4  10657  wunex3  10736  addsrpr  11070  mulsrpr  11071  recexsrlem  11098  mulcani  11853  div1  11903  recdiv  11920  divdiv1  11925  divdiv2  11926  div23i  11972  div11i  11973  divmuldivi  11974  divadddivi  11976  divdivdivi  11977  lemulge11  12076  negiso  12194  dfnn3  12226  2cnne0  12422  2rene0  12423  halfpm6th  12433  avglt1  12450  avglt2  12451  div4p1lem1div2  12467  3halfnz  12641  divlt1lt  13043  divle1le  13044  nnledivrp  13086  x2times  13278  xrsupsslem  13286  xrinfmsslem  13287  fz0to4untppr  13604  om2uzoi  13920  fzennn  13933  expge1  14065  sqoddm1div8  14206  faclbnd2  14251  faclbnd4lem1  14253  4bc2eq6  14289  hashfxnn0  14297  hashsnlei  14378  hashunlei  14385  hashsslei  14386  hash2prb  14433  repswccat  14736  cshwsexaOLD  14775  funcnvs4  14866  f1oun2prg  14868  wrdlen2i  14893  relexpaddg  15000  cjreb  15070  sqrt2gt1lt2  15221  abs1m  15282  bpoly3  16002  ege2le3  16033  efi4p  16080  efival  16095  sin01bnd  16128  cos01bnd  16129  cos1bnd  16130  cos2bnd  16131  sin01gt0  16133  cos01gt0  16134  sin02gt0  16135  sincos2sgn  16137  sin4lt0  16138  egt2lt3  16149  rpnnen2lem3  16159  rpnnen2lem11  16167  nthruc  16195  nthruz  16196  3dvdsdec  16275  3dvds2dec  16276  mod2eq1n2dvds  16290  halfleoddlt  16305  divalglem5  16340  ndvdsi  16355  flodddiv4  16356  flodddiv4lt  16358  bitsp1o  16374  3lcm2e6woprm  16552  6lcm4e12  16553  pcrec  16791  prmrec  16855  prmgaplcmlem1  16984  prmgaplcm  16993  modsubi  17005  structfn  17089  strleun  17090  slotsdifipndx  17280  slotsdifplendx  17320  slotsdifdsndx  17339  slotsdifunifndx  17346  slotsdifplendx2  17362  slotsdifocndx  17363  isofn  17722  sscres  17770  funcestrcsetclem7  18098  funcestrcsetclem8  18099  fullestrcsetc  18103  mgmnsgrpex  18812  pwmnd  18818  ga0  19162  symg2bas  19260  f1otrspeq  19315  psgnsn  19388  0frgp  19647  gsummptnn0fz  19854  srgbinomlem4  20052  cnfldfun  20956  cnfldfunALT  20957  cnfldfunALTOLD  20958  cnfld1  20970  cnsubdrglem  20996  expmhm  21014  expghm  21045  psrbag0  21623  psrbagsn  21624  coe1fsupp  21738  coe1mul2  21791  evls1sca  21842  matmulr  21940  mat1dimelbas  21973  mat1f1o  21980  m2detleib  22133  smadiadetglem1  22173  pmatcollpw3fi1lem2  22289  cpmidpmatlem2  22373  cpmadumatpolylem1  22383  cayhamlem3  22389  cayhamlem4  22390  isbasis3g  22452  fctop  22507  cctop  22509  refref  23017  bl2in  23906  dscmet  24081  iihalf1  24447  iihalf2  24449  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  iscvsi  24645  zclmncvs  24665  ncvs1  24674  ehl2eudis  24939  minveclem2  24943  minveclem4  24949  ovolunlem1a  25013  volf  25046  i1f1lem  25206  mbfi1fseqlem5  25237  dveflem  25496  pilem2  25964  pilem3  25965  sinhalfpilem  25973  sincosq1lem  26007  tangtx  26015  sinq12gt0  26017  sincos4thpi  26023  sincos6thpi  26025  sincos3rdpi  26026  pigt3  26027  pige3ALT  26029  coseq1  26034  efeq1  26037  efif1olem4  26054  angneg  26308  ang180lem1  26314  1cubrlem  26346  quart1  26361  log2cnv  26449  log2tlbnd  26450  log2ublem1  26451  log2ub  26454  emcllem1  26500  emcllem6  26505  basellem1  26585  basellem2  26586  basellem3  26587  basellem8  26592  ppiublem1  26705  ppiublem2  26706  ppiub  26707  chtublem  26714  chtub  26715  bcmono  26780  bclbnd  26783  bpos1lem  26785  bposlem1  26787  bposlem2  26788  bposlem3  26789  bposlem4  26790  bposlem5  26791  bposlem6  26792  bposlem7  26793  bposlem8  26794  bposlem9  26795  lgsdir2lem1  26828  1lgs  26843  gausslemma2dlem0c  26861  gausslemma2dlem0d  26862  gausslemma2dlem1a  26868  gausslemma2dlem2  26870  gausslemma2dlem3  26871  gausslemma2dlem5  26874  gausslemma2dlem6  26875  lgsquad2lem2  26888  2lgslem1a1  26892  2lgslem1a2  26893  2lgslem1c  26896  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2lgslem3  26907  2lgsoddprmlem1  26911  addsqrexnreu  26945  addsqnreup  26946  chebbnd1lem1  26972  chebbnd1lem3  26974  chebbnd1  26975  dchrisum0flblem2  27012  dchrisum0lem1  27019  mulog2sumlem2  27038  selberglem2  27049  chpdifbndlem1  27056  mulscl  27590  sltmul  27592  divs1  27651  precsexlem8  27660  slotsinbpsd  27692  slotslnbpsd  27693  ercgrg  27768  axlowdimlem4  28203  axlowdimlem5  28204  axlowdimlem6  28205  axlowdimlem7  28206  axlowdimlem8  28207  axlowdimlem10  28209  axlowdimlem11  28210  graop  28289  grastruct  28290  uhgrunop  28335  upgrop  28354  upgrunop  28379  umgrunop  28381  usgrop  28423  usgr2v1e2w  28509  usgrexmpldifpr  28515  usgrexmpledg  28519  uhgrsubgrself  28537  uhgrspan1lem1  28557  upgrres1lem1  28566  fusgrfis  28587  vtxd0nedgb  28745  p1evtxdeqlem  28769  p1evtxdeq  28770  p1evtxdp1  28771  umgr2v2e  28782  vdegp1bi  28794  wlkcomp  28888  upgr2pthnlp  28989  usgr2trlncl  29017  usgr2pthlem  29020  clwlkcomp  29036  uspgrn2crct  29062  wwlksonvtx  29109  wspthnonp  29113  2wlkond  29191  2pthond  29196  2pthon3v  29197  umgr2adedgwlkonALT  29201  umgr2wlk  29203  umgr2wlkon  29204  wpthswwlks2on  29215  elwspths2spth  29221  0ewlk  29367  0pth  29378  0pthonv  29382  1pthon2v  29406  3wlkdlem4  29415  3trlond  29426  3pthond  29428  3spthond  29430  trlsegvdeglem3  29475  eupthvdres  29488  eupth2lemb  29490  ex-natded5.2i  29659  ex-an  29675  ex-id  29687  ex-po  29688  ex-fl  29700  ex-mod  29702  ex-exp  29703  ex-lcm  29711  nvz0  29921  ipidsq  29963  ipdirilem  30082  siilem1  30104  minvecolem2  30128  minvecolem3  30129  minvecolem4  30133  hvsubcan  30327  hvsubcan2  30328  normlem7tALT  30372  helch  30496  hsn0elch  30501  hhshsslem2  30521  hhsssh  30522  shscli  30570  shintcli  30582  shintcl  30583  chintcli  30584  chintcl  30585  shincli  30615  shsval2i  30640  omlsi  30657  chincli  30713  chabs1  30769  fh1i  30874  fh2i  30875  cm2ji  30878  pjnormi  30974  nmopsetn0  31118  nmfnsetn0  31131  lnophm  31272  nmcexi  31279  nmbdfnlb  31303  imaelshi  31311  nlelshi  31313  nmopadjlem  31342  nmopcoadji  31354  hmopidmch  31406  hmopidmpj  31407  sto1i  31489  stlei  31493  stji1i  31495  csmdsymi  31587  chirred  31648  cdj3lem1  31687  rpdp2cl  32048  dp2lt10  32050  dp2lt  32051  dp2ltc  32053  dpfrac1  32058  dplti  32071  dpgti  32072  dpexpp1  32074  dpadd3  32078  dpmul  32079  dpmul4  32080  xrsclat  32181  nn0archi  32462  lmatfvlem  32795  xrge0iifmhm  32919  qqh0  32964  qqh1  32965  rerrext  32989  cnrrext  32990  prsiga  33129  oms0  33296  coinfliprv  33481  ballotlem1  33485  ballotth  33536  signsw0g  33567  hgt750lemd  33660  hgt750lem  33663  hgt750lem2  33664  hgt750leme  33670  tgoldbachgt  33675  subfacval2  34178  erdszelem2  34183  cvmliftlem4  34279  satom  34347  satfv1  34354  sat1el2xp  34370  fmlaomn0  34381  satfdmfmla  34391  satfv1fvfmla1  34414  ex-sategoelelomsuc  34417  ex-sategoelel12  34418  prv0  34421  prv1n  34422  elmrsubrn  34511  msubfval  34515  problem4  34653  quad3  34655  br6  34727  dfon2lem3  34757  fullfunfnv  34918  fneref  35235  filnetlem2  35264  filnetlem3  35265  onpsstopbas  35315  dnizeq0  35351  dnibndlem12  35365  knoppcnlem5  35373  knoppcnlem8  35376  knoppcnlem10  35378  knoppcnlem11  35379  knoppndvlem14  35401  cnndvlem1  35413  bj-genr  35484  bj-genl  35485  bj-genan  35486  bj-2upln1upl  35905  bj-vtoclgfALT  35940  bj-brab2a1  36030  bj-opabssvv  36031  taupilem1  36202  topdifinf  36230  sin2h  36478  cos2h  36479  tan2h  36480  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem11  36499  poimirlem12  36500  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem29  36517  poimirlem31  36519  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  itg2addnclem2  36540  asindmre  36571  heiborlem7  36685  riscer  36856  refrelcoss3  37333  symrelcoss3  37335  ishlatiN  38225  0psubN  38620  atpsubN  38624  gcdcomnni  40854  gcdnegnni  40855  neggcdnni  40856  60gcd7e1  40870  lcmeprodgcdi  40872  lcm2un  40879  lcm3un  40880  lcmineqlem4  40897  lcmineqlem6  40899  3lexlogpow5ineq1  40919  aks4d1p1p2  40935  mzpclall  41465  diophin  41510  diophun  41511  eldioph4b  41549  irrapx1  41566  2nn0ind  41684  aomclem4  41799  onexlimgt  41992  nnoeomeqom  42062  oaomoencom  42067  oenassex  42068  succlg  42078  dflim5  42079  omabs2  42082  tfsconcatfv2  42090  ifpid3g  42243  ifpid2g  42244  ifpbi1b  42254  eu0  42271  pwinfi  42315  rtrclex  42368  cnvrcl0  42376  dfrcl2  42425  relexp1idm  42465  relexp0idm  42466  clsk1independent  42797  lhe4.4ex1a  43088  expgrowth  43094  ax6e2nd  43319  uun0.1  43539  relopabVD  43662  ax6e2ndVD  43669  sb5ALTVD  43674  ax6e2ndALT  43691  rexanuz2nf  44203  dvmptconst  44631  dvmptidg  44633  dvmulcncf  44641  dvdivcncf  44643  dvnprodlem3  44664  itgsinexplem1  44670  volioof  44703  stoweidlem13  44729  stoweidlem14  44730  stoweidlem26  44742  stoweidlem34  44750  stoweidlem49  44765  stoweidlem59  44775  dirkertrigeqlem3  44816  dirkercncflem1  44819  dirkercncflem2  44820  fourierdlem57  44879  fourierdlem62  44884  fourierdlem103  44925  fourierdlem111  44933  fourierswlem  44946  fouriersw  44947  salexct2  45055  salexct3  45058  salgencntex  45059  salgensscntex  45060  gsumge0cl  45087  sge00  45092  sge0tsms  45096  0ome  45245  ovnlecvr  45274  ovn0lem  45281  hoidmvle  45316  ovnsubadd2lem  45361  smflimlem6  45492  mbfpsssmf  45499  smfmullem4  45510  smfpimbor1lem1  45514  astbstanbst  45619  aistbistaandb  45620  abnotataxb  45626  aifftbifffaibif  45631  confun4  45652  plcofph  45654  plvcofph  45656  plvcofphax  45657  plvofpos  45658  mdandyv0  45659  mdandyv1  45660  mdandyv2  45661  mdandyv3  45662  mdandyv4  45663  mdandyv5  45664  mdandyv6  45665  mdandyv7  45666  mdandyv8  45667  mdandyv9  45668  mdandyv10  45669  mdandyv11  45670  mdandyv12  45671  mdandyv13  45672  mdandyv14  45673  mdandyv15  45674  mdandyvr0  45675  mdandyvr1  45676  mdandyvr2  45677  mdandyvr3  45678  mdandyvr4  45679  mdandyvr5  45680  mdandyvr6  45681  mdandyvr7  45682  mdandyvrx0  45691  mdandyvrx1  45692  mdandyvrx2  45693  mdandyvrx3  45694  mdandyvrx4  45695  mdandyvrx5  45696  mdandyvrx6  45697  mdandyvrx7  45698  dandysum2p2e4  45708  or2expropbilem1  45742  dfnelbr2  45981  ich2exprop  46139  paireqne  46179  fmtno4prmfac  46240  31prm  46265  lighneallem4a  46276  41prothprmlem2  46286  zofldiv2ALTV  46330  nfermltl8rev  46410  nfermltl2rev  46411  nfermltlrev  46412  gbegt5  46429  gbowgt5  46430  gboge9  46432  9gbo  46442  11gbo  46443  nnsum3primes4  46456  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  tgblthelfgott  46483  tgoldbach  46485  isomgrref  46503  ushrisomgr  46509  nn0mnd  46589  mgmplusgiopALT  46604  sgrp2sgrp  46638  isrnghm  46690  pzriprnglem4  46808  pzriprnglem9  46813  pzriprnglem14  46818  pzriprng1ALT  46820  2zrngaabl  46842  rnghmsscmap2  46871  rnghmsscmap  46872  funcrngcsetc  46896  funcrngcsetcALT  46897  rhmsscmap2  46917  rhmsscmap  46918  funcringcsetc  46933  funcringcsetcALTV2lem8  46941  funcringcsetclem8ALTV  46964  zlmodzxzlmod  47030  zlmodzxzel  47031  zlmodzxzscm  47033  zlmodzxzadd  47034  snlindsntorlem  47151  ldepspr  47154  lmod1lem2  47169  lmod1lem3  47170  lmod1lem4  47171  lmod1lem5  47172  lmodn0  47176  zlmodzxznm  47178  zlmodzxzldeplem  47179  zlmodzxzldeplem1  47181  zlmodzxzldeplem3  47183  lvecpsslmod  47188  ldepsnlinc  47189  ldepslinc  47190  expnegico01  47199  zofldiv2  47217  flnn0div2ge  47219  elbigo2  47238  nnlog2ge0lt1  47252  digfval  47283  dignnld  47289  dignn0flhalf  47304  2arymaptfo  47340  itcovalt2lem1  47361  prelrrx2  47399  eenglngeehlnmlem2  47424  rrxsphere  47434  line2  47438  line2x  47440  line2y  47441  itsclc0yqsollem2  47449  inlinecirc02plem  47472  sepfsepc  47560  alimp-surprise  47827  aacllem  47848