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  4141  ssini  4190  opthhausdorff  5457  elvv  5691  elopaelxp  5706  relopabiv  5760  relopabi  5762  dfpo2  6243  funpr  6537  funcnvpr  6543  mpov  7458  caovcom  7543  snnex  7691  pwnex  7692  1st2val  7949  2nd2val  7950  elxp7  7956  opreuopreu  7966  poxp2  8073  poseq  8088  tfr1a  8313  oeoa  8512  oeoe  8514  erov  8738  endisj  8977  snopfsupp  9275  ssttrcl  9605  ttrclselem2  9616  r1funlim  9656  dfac2b  10019  cflecard  10141  canth4  10535  canthnumlem  10536  canthwelem  10538  canthp1lem2  10541  pwfseqlem4  10550  wunex3  10629  addsrpr  10963  mulsrpr  10964  recexsrlem  10991  mulcani  11753  div1  11808  recdiv  11824  divdiv1  11829  divdiv2  11830  div23i  11876  div11i  11877  divmuldivi  11878  divadddivi  11880  divdivdivi  11881  lemulge11  11981  negiso  12099  dfnn3  12136  2cnne0  12327  2rene0  12328  halfpm6th  12340  avglt1  12356  avglt2  12357  div4p1lem1div2  12373  3halfnz  12549  divlt1lt  12958  divle1le  12959  nnledivrp  13001  x2times  13195  xrsupsslem  13203  xrinfmsslem  13204  fvf1tp  13690  om2uzoi  13859  fzennn  13872  expge1  14003  sqoddm1div8  14147  faclbnd2  14195  faclbnd4lem1  14197  4bc2eq6  14233  hashfxnn0  14241  hashsnlei  14322  hashunlei  14329  hashsslei  14330  hash2prb  14376  repswccat  14690  funcnvs4  14819  f1oun2prg  14821  wrdlen2i  14846  s2rn  14867  s3rn  14868  s7rn  14869  relexpaddg  14957  cjreb  15027  sqrt2gt1lt2  15178  abs1m  15240  bpoly3  15962  ege2le3  15994  efi4p  16043  efival  16058  sin01bnd  16091  cos01bnd  16092  cos1bnd  16093  cos2bnd  16094  sin01gt0  16096  cos01gt0  16097  sin02gt0  16098  sincos2sgn  16100  sin4lt0  16101  egt2lt3  16112  rpnnen2lem3  16122  rpnnen2lem11  16130  nthruc  16158  nthruz  16159  3dvdsdec  16240  3dvds2dec  16241  mod2eq1n2dvds  16255  halfleoddlt  16270  divalglem5  16305  ndvdsi  16320  flodddiv4  16323  flodddiv4lt  16325  bitsp1o  16341  3lcm2e6woprm  16523  6lcm4e12  16524  pcrec  16767  prmrec  16831  prmgaplcmlem1  16960  prmgaplcm  16969  modsubi  16981  structfn  17064  strleun  17065  slotsdifipndx  17236  slotsdifplendx  17276  slotsdifdsndx  17295  slotsdifunifndx  17302  slotsdifplendx2  17317  slotsdifocndx  17318  isofn  17679  sscres  17727  funcestrcsetclem7  18049  funcestrcsetclem8  18050  fullestrcsetc  18054  nulchn  18522  chninf  18538  mgmnsgrpex  18836  pwmnd  18842  ga0  19208  symg2bas  19303  f1otrspeq  19357  psgnsn  19430  0frgp  19689  gsummptnn0fz  19896  srgbinomlem4  20145  isrnghm  20357  rnghmsscmap2  20542  rnghmsscmap  20543  funcrngcsetc  20553  funcrngcsetcALT  20554  rhmsscmap2  20571  rhmsscmap  20572  funcringcsetc  20587  cnfldfun  21303  cnfldfunALT  21304  cnfldfunOLD  21316  cnfldfunALTOLD  21317  cnfld1  21328  cnfld1OLD  21329  cnsubdrglem  21353  expmhm  21371  expghm  21410  pzriprnglem4  21419  pzriprnglem9  21424  pzriprnglem14  21429  pzriprng1ALT  21431  psrbag0  21995  psrbagsn  21996  coe1fsupp  22125  coe1mul2  22181  evls1sca  22236  matmulr  22351  mat1dimelbas  22384  mat1f1o  22391  m2detleib  22544  smadiadetglem1  22584  pmatcollpw3fi1lem2  22700  cpmidpmatlem2  22784  cpmadumatpolylem1  22794  cayhamlem3  22800  cayhamlem4  22801  isbasis3g  22862  fctop  22917  cctop  22919  refref  23426  bl2in  24313  dscmet  24485  iihalf1  24850  iihalf2  24853  icopnfhmeo  24866  iccpnfhmeo  24868  xrhmeo  24869  iscvsi  25054  zclmncvs  25073  ncvs1  25082  ehl2eudis  25347  minveclem2  25351  minveclem4  25357  ovolunlem1a  25422  volf  25455  i1f1lem  25615  mbfi1fseqlem5  25645  dveflem  25908  pilem2  26387  pilem3  26388  sinhalfpilem  26397  sincosq1lem  26431  tangtx  26439  sinq12gt0  26441  sincos4thpi  26447  sincos6thpi  26450  sincos3rdpi  26451  pigt3  26452  pige3ALT  26454  coseq1  26459  efeq1  26462  efif1olem4  26479  angneg  26738  ang180lem1  26744  1cubrlem  26776  quart1  26791  log2cnv  26879  log2tlbnd  26880  log2ublem1  26881  log2ub  26884  emcllem1  26931  emcllem6  26936  basellem1  27016  basellem2  27017  basellem3  27018  basellem8  27023  ppiublem1  27138  ppiublem2  27139  ppiub  27140  chtublem  27147  chtub  27148  bcmono  27213  bclbnd  27216  bpos1lem  27218  bposlem1  27220  bposlem2  27221  bposlem3  27222  bposlem4  27223  bposlem5  27224  bposlem6  27225  bposlem7  27226  bposlem8  27227  bposlem9  27228  lgsdir2lem1  27261  1lgs  27276  gausslemma2dlem0c  27294  gausslemma2dlem0d  27295  gausslemma2dlem1a  27301  gausslemma2dlem2  27303  gausslemma2dlem3  27304  gausslemma2dlem5  27307  gausslemma2dlem6  27308  lgsquad2lem2  27321  2lgslem1a1  27325  2lgslem1a2  27326  2lgslem1c  27329  2lgslem3a  27332  2lgslem3b  27333  2lgslem3c  27334  2lgslem3d  27335  2lgslem3  27340  2lgsoddprmlem1  27344  addsqrexnreu  27378  addsqnreup  27379  chebbnd1lem1  27405  chebbnd1lem3  27407  chebbnd1  27408  dchrisum0flblem2  27445  dchrisum0lem1  27452  mulog2sumlem2  27471  selberglem2  27482  chpdifbndlem1  27489  ssltsnb  27730  mulscl  28071  sltmul  28073  divs1  28141  precsexlem8  28150  0reno  28397  slotsinbpsd  28417  slotslnbpsd  28418  ercgrg  28493  axlowdimlem4  28921  axlowdimlem5  28922  axlowdimlem6  28923  axlowdimlem7  28924  axlowdimlem8  28925  axlowdimlem10  28927  axlowdimlem11  28928  graop  29005  grastruct  29006  uhgrunop  29051  upgrop  29070  upgrunop  29095  umgrunop  29097  usgrop  29139  usgr2v1e2w  29228  usgrexmpldifpr  29234  usgrexmpledg  29238  uhgrsubgrself  29256  uhgrspan1lem1  29276  upgrres1lem1  29285  fusgrfis  29306  vtxd0nedgb  29465  p1evtxdeqlem  29489  p1evtxdeq  29490  p1evtxdp1  29491  umgr2v2e  29502  vdegp1bi  29514  wlkcomp  29607  upgr2pthnlp  29708  usgr2trlncl  29736  usgr2pthlem  29739  clwlkcomp  29755  uspgrn2crct  29784  wwlksonvtx  29831  wspthnonp  29835  2wlkond  29913  2pthond  29918  2pthon3v  29919  umgr2adedgwlkonALT  29923  umgr2wlk  29925  umgr2wlkon  29926  wpthswwlks2on  29937  elwspths2spth  29943  0ewlk  30089  0pth  30100  0pthonv  30104  1pthon2v  30128  3wlkdlem4  30137  3trlond  30148  3pthond  30150  3spthond  30152  trlsegvdeglem3  30197  eupthvdres  30210  eupth2lemb  30212  ex-natded5.2i  30381  ex-an  30397  ex-id  30409  ex-po  30410  ex-fl  30422  ex-mod  30424  ex-exp  30425  ex-lcm  30433  nvz0  30643  ipidsq  30685  ipdirilem  30804  siilem1  30826  minvecolem2  30850  minvecolem3  30851  minvecolem4  30855  hvsubcan  31049  hvsubcan2  31050  normlem7tALT  31094  helch  31218  hsn0elch  31223  hhshsslem2  31243  hhsssh  31244  shscli  31292  shintcli  31304  shintcl  31305  chintcli  31306  chintcl  31307  shincli  31337  shsval2i  31362  omlsi  31379  chincli  31435  chabs1  31491  fh1i  31596  fh2i  31597  cm2ji  31600  pjnormi  31696  nmopsetn0  31840  nmfnsetn0  31853  lnophm  31994  nmcexi  32001  nmbdfnlb  32025  imaelshi  32033  nlelshi  32035  nmopadjlem  32064  nmopcoadji  32076  hmopidmch  32128  hmopidmpj  32129  sto1i  32211  stlei  32215  stji1i  32217  csmdsymi  32309  chirred  32370  cdj3lem1  32409  rpdp2cl  32857  dp2lt10  32859  dp2lt  32860  dp2ltc  32862  dpfrac1  32867  dplti  32880  dpgti  32881  dpexpp1  32883  dpadd3  32887  dpmul  32888  dpmul4  32889  xrsclat  32987  nn0archi  33307  zringfrac  33514  cos9thpiminplylem4  33793  cos9thpiminplylem5  33794  cos9thpinconstr  33799  lmatfvlem  33823  xrge0iifmhm  33947  qqh0  33992  qqh1  33993  rerrext  34017  cnrrext  34018  prsiga  34139  oms0  34305  coinfliprv  34491  ballotlem1  34495  ballotth  34546  signsw0g  34564  hgt750lemd  34656  hgt750lem  34659  hgt750lem2  34660  hgt750leme  34666  tgoldbachgt  34671  subfacval2  35219  erdszelem2  35224  cvmliftlem4  35320  satom  35388  satfv1  35395  sat1el2xp  35411  fmlaomn0  35422  satfdmfmla  35432  satfv1fvfmla1  35455  ex-sategoelelomsuc  35458  ex-sategoelel12  35459  prv0  35462  prv1n  35463  elmrsubrn  35552  msubfval  35556  problem4  35700  quad3  35702  br6  35789  dfon2lem3  35818  fullfunfnv  35979  itgeq12i  36239  fneref  36383  filnetlem2  36412  filnetlem3  36413  onpsstopbas  36463  dnizeq0  36508  dnibndlem12  36522  knoppcnlem5  36530  knoppcnlem8  36533  knoppcnlem11  36536  knoppndvlem14  36558  cnndvlem1  36570  bj-genr  36639  bj-genl  36640  bj-genan  36641  bj-2upln1upl  37057  bj-vtoclgfALT  37092  bj-brab2a1  37182  bj-opabssvv  37183  taupilem1  37354  topdifinf  37382  sin2h  37649  cos2h  37650  tan2h  37651  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem6  37665  poimirlem7  37666  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem23  37682  poimirlem24  37683  poimirlem25  37684  poimirlem26  37685  poimirlem29  37688  poimirlem31  37690  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  itg2addnclem2  37711  asindmre  37742  heiborlem7  37856  riscer  38027  refrelcoss3  38499  symrelcoss3  38501  ishlatiN  39393  0psubN  39787  atpsubN  39791  gcdcomnni  42020  gcdnegnni  42021  neggcdnni  42022  60gcd7e1  42037  lcmeprodgcdi  42039  lcm2un  42046  lcm3un  42047  lcmineqlem4  42064  lcmineqlem6  42066  3lexlogpow5ineq1  42086  aks4d1p1p2  42102  mzpclall  42759  diophin  42804  diophun  42805  eldioph4b  42843  irrapx1  42860  2nn0ind  42977  aomclem4  43089  onexlimgt  43275  nnoeomeqom  43344  oaomoencom  43349  oenassex  43350  succlg  43360  dflim5  43361  omabs2  43364  tfsconcatfv2  43372  ifpid3g  43524  ifpid2g  43525  ifpbi1b  43535  eu0  43552  pwinfi  43596  rtrclex  43649  cnvrcl0  43657  dfrcl2  43706  relexp1idm  43746  relexp0idm  43747  clsk1independent  44078  lhe4.4ex1a  44361  expgrowth  44367  ax6e2nd  44590  uun0.1  44809  relopabVD  44932  ax6e2ndVD  44939  sb5ALTVD  44944  ax6e2ndALT  44961  permaxinf2lem  45044  rexanuz2nf  45529  dvmptconst  45952  dvmptidg  45954  dvmulcncf  45962  dvdivcncf  45964  dvnprodlem3  45985  itgsinexplem1  45991  volioof  46024  stoweidlem13  46050  stoweidlem14  46051  stoweidlem26  46063  stoweidlem34  46071  stoweidlem49  46086  stoweidlem59  46096  dirkertrigeqlem3  46137  dirkercncflem1  46140  dirkercncflem2  46141  fourierdlem57  46200  fourierdlem62  46205  fourierdlem103  46246  fourierdlem111  46254  fourierswlem  46267  fouriersw  46268  salexct2  46376  salexct3  46379  salgencntex  46380  salgensscntex  46381  gsumge0cl  46408  sge00  46413  sge0tsms  46417  0ome  46566  ovnlecvr  46595  ovn0lem  46602  hoidmvle  46637  ovnsubadd2lem  46682  smflimlem6  46813  mbfpsssmf  46820  smfmullem4  46831  smfpimbor1lem1  46835  cjnpoly  46919  sinnpoly  46921  astbstanbst  46939  aistbistaandb  46940  abnotataxb  46946  aifftbifffaibif  46951  confun4  46972  plcofph  46974  plvcofph  46976  plvcofphax  46977  plvofpos  46978  mdandyv0  46979  mdandyv1  46980  mdandyv2  46981  mdandyv3  46982  mdandyv4  46983  mdandyv5  46984  mdandyv6  46985  mdandyv7  46986  mdandyv8  46987  mdandyv9  46988  mdandyv10  46989  mdandyv11  46990  mdandyv12  46991  mdandyv13  46992  mdandyv14  46993  mdandyv15  46994  mdandyvr0  46995  mdandyvr1  46996  mdandyvr2  46997  mdandyvr3  46998  mdandyvr4  46999  mdandyvr5  47000  mdandyvr6  47001  mdandyvr7  47002  mdandyvrx0  47011  mdandyvrx1  47012  mdandyvrx2  47013  mdandyvrx3  47014  mdandyvrx4  47015  mdandyvrx5  47016  mdandyvrx6  47017  mdandyvrx7  47018  dandysum2p2e4  47028  or2expropbilem1  47062  dfnelbr2  47303  2ltceilhalf  47358  ich2exprop  47501  paireqne  47541  fmtno4prmfac  47602  31prm  47627  lighneallem4a  47638  41prothprmlem2  47648  zofldiv2ALTV  47692  nfermltl8rev  47772  nfermltl2rev  47773  nfermltlrev  47774  gbegt5  47791  gbowgt5  47792  gboge9  47794  9gbo  47804  11gbo  47805  nnsum3primes4  47818  nnsum3primesgbe  47822  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  tgblthelfgott  47845  tgoldbach  47847  ushggricedg  47957  isubgrgrim  47959  stgrvtx  47984  stgriedg  47985  stgrusgra  47989  stgr1  47991  uspgrlim  48022  grlimprclnbgrvtx  48029  clnbgr3stgrgrlic  48050  usgrexmpl1lem  48051  usgrexmpl2lem  48056  usgrexmpl2nb0  48061  usgrexmpl2nb1  48062  usgrexmpl2nb2  48063  usgrexmpl2nb3  48064  usgrexmpl2nb4  48065  usgrexmpl2nb5  48066  gpgvtx  48073  gpgiedg  48074  gpgorder  48089  gpgvtxedg0  48093  gpgvtxedg1  48094  gpgedgiov  48095  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpg3kgrtriexlem3  48115  gpg3kgrtriexlem6  48118  gpgprismgr4cycllem2  48126  gpgprismgr4cyclex  48137  pgnioedg1  48138  pgnioedg2  48139  pgnioedg3  48140  pgnioedg4  48141  pgnioedg5  48142  pgnbgreunbgrlem2lem1  48144  pgnbgreunbgrlem2lem2  48145  pgnbgreunbgrlem2lem3  48146  pgnbgreunbgrlem3  48148  pgnbgreunbgrlem4  48149  pgnbgreunbgrlem5lem1  48150  pgnbgreunbgrlem5lem2  48151  pgnbgreunbgrlem5lem3  48152  pgnbgreunbgrlem6  48154  gpg5ngric  48158  gpg5edgnedg  48160  nn0mnd  48209  mgmplusgiopALT  48224  sgrp2sgrp  48258  2zrngaabl  48280  funcringcsetcALTV2lem8  48327  funcringcsetclem8ALTV  48350  zlmodzxzlmod  48384  zlmodzxzel  48385  zlmodzxzscm  48387  zlmodzxzadd  48388  snlindsntorlem  48501  ldepspr  48504  lmod1lem2  48519  lmod1lem3  48520  lmod1lem4  48521  lmod1lem5  48522  lmodn0  48526  zlmodzxznm  48528  zlmodzxzldeplem  48529  zlmodzxzldeplem1  48531  zlmodzxzldeplem3  48533  lvecpsslmod  48538  ldepsnlinc  48539  ldepslinc  48540  expnegico01  48549  zofldiv2  48562  flnn0div2ge  48564  elbigo2  48583  nnlog2ge0lt1  48597  digfval  48628  dignnld  48634  dignn0flhalf  48649  2arymaptfo  48685  itcovalt2lem1  48706  prelrrx2  48744  eenglngeehlnmlem2  48769  rrxsphere  48779  line2  48783  line2x  48785  line2y  48786  itsclc0yqsollem2  48794  inlinecirc02plem  48817  sepfsepc  48958  invfn  49061  alimp-surprise  49811  aacllem  49832