Theorem pm3.2i 475

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

Syntax hints:   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mp4an  705  pm4.87  856  3pm3.2i  1358  unssi  4145  ssini  4193  opthhausdorff  5502  elvv  5738  elopaelxp  5753  relopabiv  5809  relopabi  5811  dfpo2  6299  funpr  6594  funcnvpr  6600  mpov  7524  caovcom  7609  snnex  7758  pwnex  7759  1st2val  8015  2nd2val  8016  elxp7  8022  opreuopreu  8032  poxp2  8140  poseq  8155  tfr1a  8382  oeoa  8584  oeoe  8586  erov  8813  endisj  9053  snopfsupp  9352  ssttrcl  9685  ttrclselem2  9696  r1funlim  9739  dfac2b  10115  cflecard  10237  canth4  10633  canthnumlem  10634  canthwelem  10636  canthp1lem2  10639  pwfseqlem4  10648  wunex3  10727  addsrpr  11061  mulsrpr  11062  recexsrlem  11089  mulcani  11854  div1  11905  recdiv  11922  divdiv1  11927  divdiv2  11928  div23i  11974  div11i  11975  divmuldivi  11976  divadddivi  11978  divdivdivi  11979  lemulge11  12078  negiso  12196  dfnn3  12248  2cnne0  12454  2rene0  12455  halfpm6th  12467  avglt1  12483  avglt2  12484  div4p1lem1div2  12500  3halfnz  12676  divlt1lt  13088  divle1le  13089  nnledivrp  13131  x2times  13326  xrsupsslem  13334  xrinfmsslem  13335  nnge2recico01  13535  fvf1tp  13824  om2uzoi  13993  fzennn  14006  expge1  14137  sqoddm1div8  14281  faclbnd2  14329  faclbnd4lem1  14331  4bc2eq6  14367  hashfxnn0  14375  hashsnlei  14457  hashunlei  14464  hashsslei  14465  hash2prb  14511  repswccat  14825  funcnvs4  14954  f1oun2prg  14956  wrdlen2i  14981  s2rn  15002  s3rn  15003  s7rn  15004  relexpaddg  15092  cjreb  15176  sqrt2gt1lt2  15327  abs1m  15389  bpoly3  16113  ege2le3  16145  efi4p  16194  efival  16209  sin01bnd  16242  cos01bnd  16243  cos1bnd  16244  cos2bnd  16245  sin01gt0  16247  cos01gt0  16248  sin02gt0  16249  sincos2sgn  16251  sin4lt0  16252  egt2lt3  16263  rpnnen2lem3  16273  rpnnen2lem11  16281  nthruc  16309  nthruz  16310  3dvdsdec  16391  3dvds2dec  16392  mod2eq1n2dvds  16406  halfleoddlt  16421  divalglem5  16456  ndvdsi  16471  flodddiv4  16474  flodddiv4lt  16476  bitsp1o  16492  3lcm2e6woprm  16674  6lcm4e12  16675  pcrec  16919  prmrec  16983  prmgaplcmlem1  17112  prmgaplcm  17121  modsubi  17133  structfn  17217  strleun  17218  slotsdifipndx  17389  slotsdifplendx  17429  slotsdifdsndx  17448  slotsdifunifndx  17455  slotsdifplendx2  17470  slotsdifocndx  17471  isofn  17833  sscres  17881  funcestrcsetclem7  18203  funcestrcsetclem8  18204  fullestrcsetc  18208  nulchn  18676  chninf  18692  mgmnsgrpex  18994  pwmnd  19000  ga0  19369  symg2bas  19464  f1otrspeq  19518  psgnsn  19591  0frgp  19850  gsummptnn0fz  20057  srgbinomlem4  20312  isrnghm  20524  rnghmsscmap2  20715  rnghmsscmap  20716  funcrngcsetc  20726  funcrngcsetcALT  20727  rhmsscmap2  20744  rhmsscmap  20745  funcringcsetc  20760  cnfldfun  21517  cnfldfunALT  21518  cnfld1  21528  cnsubdrglem  21549  expmhm  21567  expghm  21606  pzriprnglem4  21615  pzriprnglem9  21620  pzriprnglem14  21625  pzriprng1ALT  21627  psrbag0  22194  psrbagsn  22195  coe1fsupp  22355  coe1mul2  22411  evls1sca  22464  matmulr  22576  mat1dimelbas  22609  mat1f1o  22616  m2detleib  22769  smadiadetglem1  22809  pmatcollpw3fi1lem2  22925  cpmidpmatlem2  23009  cpmadumatpolylem1  23019  cayhamlem3  23025  cayhamlem4  23026  isbasis3g  23087  fctop  23142  cctop  23144  refref  23651  bl2in  24538  dscmet  24710  iihalf1  25071  iihalf2  25073  icopnfhmeo  25083  iccpnfhmeo  25085  xrhmeo  25086  iscvsi  25269  zclmncvs  25288  ncvs1  25297  ehl2eudis  25562  minveclem2  25566  minveclem4  25572  ovolunlem1a  25636  volf  25669  i1f1lem  25829  mbfi1fseqlem5  25859  dveflem  26119  pilem2  26596  pilem3  26597  sinhalfpilem  26609  sincosq1lem  26643  tangtx  26651  sinq12gt0  26653  sincos4thpi  26659  sincos6thpi  26662  sincos3rdpi  26663  pigt3  26664  pige3ALT  26666  coseq1  26671  efeq1  26674  efif1olem4  26691  angneg  26949  ang180lem1  26955  1cubrlem  26987  quart1  27002  log2cnv  27090  log2tlbnd  27091  log2ublem1  27092  log2ub  27095  emcllem1  27141  emcllem6  27146  basellem1  27226  basellem2  27227  basellem3  27228  basellem8  27233  ppiublem1  27347  ppiublem2  27348  ppiub  27349  chtublem  27356  chtub  27357  bcmono  27422  bclbnd  27425  bpos1lem  27427  bposlem1  27429  bposlem2  27430  bposlem3  27431  bposlem4  27432  bposlem5  27433  bposlem6  27434  bposlem7  27435  bposlem8  27436  bposlem9  27437  lgsdir2lem1  27470  1lgs  27485  gausslemma2dlem0c  27503  gausslemma2dlem0d  27504  gausslemma2dlem1a  27510  gausslemma2dlem2  27512  gausslemma2dlem3  27513  gausslemma2dlem5  27516  gausslemma2dlem6  27517  lgsquad2lem2  27530  2lgslem1a1  27534  2lgslem1a2  27535  2lgslem1c  27538  2lgslem3a  27541  2lgslem3b  27542  2lgslem3c  27543  2lgslem3d  27544  2lgslem3  27549  2lgsoddprmlem1  27553  addsqrexnreu  27587  addsqnreup  27588  chebbnd1lem1  27614  chebbnd1lem3  27616  chebbnd1  27617  dchrisum0flblem2  27654  dchrisum0lem1  27661  mulog2sumlem2  27680  selberglem2  27691  chpdifbndlem1  27698  sltssnb  27943  mulscl  28308  ltmuls  28310  divs1  28378  precsexlem8  28388  0reno  28670  1reno  28671  slotsinbpsd  28691  slotslnbpsd  28692  ercgrg  28767  axlowdimlem4  29276  axlowdimlem5  29277  axlowdimlem6  29278  axlowdimlem7  29279  axlowdimlem8  29280  axlowdimlem10  29282  axlowdimlem11  29283  graop  29360  grastruct  29361  uhgrunop  29406  upgrop  29425  upgrunop  29450  umgrunop  29452  usgrop  29494  usgr2v1e2w  29583  usgrexmpldifpr  29589  usgrexmpledg  29593  uhgrsubgrself  29611  uhgrspan1lem1  29631  upgrres1lem1  29640  fusgrfis  29661  vtxd0nedgb  29819  p1evtxdeqlem  29843  p1evtxdeq  29844  p1evtxdp1  29845  umgr2v2e  29856  vdegp1bi  29868  wlkcomp  29961  upgr2pthnlp  30062  usgr2trlncl  30090  usgr2pthlem  30093  clwlkcomp  30109  uspgrn2crct  30138  wwlksonvtx  30185  wspthnonp  30189  2wlkond  30267  2pthond  30272  2pthon3v  30273  umgr2adedgwlkonALT  30277  umgr2wlk  30279  umgr2wlkon  30280  wpthswwlks2on  30294  elwspths2spth  30300  0ewlk  30446  0pth  30457  0pthonv  30461  1pthon2v  30485  3wlkdlem4  30494  3trlond  30505  3pthond  30507  3spthond  30509  trlsegvdeglem3  30554  eupthvdres  30567  eupth2lemb  30569  ex-natded5.2i  30738  ex-an  30754  ex-id  30766  ex-po  30767  ex-fl  30779  ex-mod  30781  ex-exp  30782  ex-lcm  30790  nvz0  31001  ipidsq  31043  ipdirilem  31162  siilem1  31184  minvecolem2  31208  minvecolem3  31209  minvecolem4  31213  hvsubcan  31407  hvsubcan2  31408  normlem7tALT  31452  helch  31576  hsn0elch  31581  hhshsslem2  31601  hhsssh  31602  shscli  31650  shintcli  31662  shintcl  31663  chintcli  31664  chintcl  31665  shincli  31695  shsval2i  31720  omlsi  31737  chincli  31793  chabs1  31849  fh1i  31954  fh2i  31955  cm2ji  31958  pjnormi  32054  nmopsetn0  32198  nmfnsetn0  32211  lnophm  32352  nmcexi  32359  nmbdfnlb  32383  imaelshi  32391  nlelshi  32393  nmopadjlem  32422  nmopcoadji  32434  hmopidmch  32486  hmopidmpj  32487  sto1i  32569  stlei  32573  stji1i  32575  csmdsymi  32667  chirred  32728  cdj3lem1  32767  rpdp2cl  33182  dp2lt10  33184  dp2lt  33185  dp2ltc  33187  dpfrac1  33192  dplti  33205  dpgti  33206  dpexpp1  33208  dpadd3  33212  dpmul  33213  dpmul4  33214  xrsclat  33312  nn0archi  33648  zringfrac  33825  cos9thpiminplylem4  34156  cos9thpiminplylem5  34157  cos9thpinconstr  34162  lmatfvlem  34186  xrge0iifmhm  34310  qqh0  34355  qqh1  34356  rerrext  34380  cnrrext  34381  prsiga  34502  oms0  34668  coinfliprv  34854  ballotlem1  34858  ballotth  34909  signsw0g  34924  hgt750lemd  35016  hgt750lem  35019  hgt750lem2  35020  hgt750leme  35026  tgoldbachgt  35031  subfacval2  35660  erdszelem2  35665  cvmliftlem4  35761  satom  35829  satfv1  35836  sat1el2xp  35852  fmlaomn0  35863  satfdmfmla  35873  satfv1fvfmla1  35896  ex-sategoelelomsuc  35899  ex-sategoelel12  35900  prv0  35903  prv1n  35904  elmrsubrn  35993  msubfval  35997  problem4  36141  quad3  36143  br6  36230  dfon2lem3  36256  fullfunfnv  36419  itgeq12i  36699  fneref  36842  filnetlem2  36871  filnetlem3  36872  onpsstopbas  36922  dfttc3gw  37015  dfttc4lem2  37021  dnizeq0  37045  dnibndlem12  37059  knoppcnlem5  37067  knoppcnlem8  37070  knoppcnlem11  37073  knoppndvlem14  37095  cnndvlem1  37107  bj-genr  37181  bj-genl  37182  bj-genan  37183  bj-2upln1upl  37641  bj-vtoclgfALT  37676  bj-brab2a1  37774  bj-opabssvv  37775  taupilem1  37946  qdiff  37952  topdifinf  37976  sin2h  38242  cos2h  38243  tan2h  38244  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem11  38263  poimirlem12  38264  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem22  38274  poimirlem23  38275  poimirlem24  38276  poimirlem25  38277  poimirlem26  38278  poimirlem29  38281  poimirlem31  38283  mblfinlem3  38291  mblfinlem4  38292  ismblfin  38293  itg2addnclem2  38304  asindmre  38335  heiborlem7  38449  riscer  38620  refrelcoss3  39183  symrelcoss3  39185  ishlatiN  40110  0psubN  40504  atpsubN  40508  gcdcomnni  42736  gcdnegnni  42737  neggcdnni  42738  60gcd7e1  42753  lcmeprodgcdi  42755  lcm2un  42762  lcm3un  42763  lcmineqlem4  42780  lcmineqlem6  42782  3lexlogpow5ineq1  42802  aks4d1p1p2  42818  25or6to4  42954  mzpclall  43441  diophin  43486  diophun  43487  eldioph4b  43521  irrapx1  43538  2nn0ind  43655  aomclem4  43767  onexlimgt  43953  nnoeomeqom  44022  oaomoencom  44027  oenassex  44028  succlg  44038  dflim5  44039  omabs2  44042  tfsconcatfv2  44050  ifpid3g  44201  ifpid2g  44202  ifpbi1b  44212  eu0  44229  pwinfi  44273  rtrclex  44326  cnvrcl0  44334  dfrcl2  44383  relexp1idm  44423  relexp0idm  44424  clsk1independent  44755  lhe4.4ex1a  45022  expgrowth  45028  ax6e2nd  45250  uun0.1  45469  relopabVD  45592  ax6e2ndVD  45599  sb5ALTVD  45604  ax6e2ndALT  45621  permaxinf2lem  45704  rexanuz2nf  46189  dvmptconst  46612  dvmptidg  46614  dvmulcncf  46622  dvdivcncf  46624  dvnprodlem3  46645  itgsinexplem1  46651  volioof  46684  stoweidlem13  46710  stoweidlem14  46711  stoweidlem26  46723  stoweidlem34  46731  stoweidlem49  46746  stoweidlem59  46756  dirkertrigeqlem3  46797  dirkercncflem1  46800  dirkercncflem2  46801  fourierdlem57  46860  fourierdlem62  46865  fourierdlem103  46906  fourierdlem111  46914  fourierswlem  46927  fouriersw  46928  salexct2  47036  salexct3  47039  salgencntex  47040  salgensscntex  47041  gsumge0cl  47068  sge00  47073  sge0tsms  47077  0ome  47226  ovnlecvr  47255  ovn0lem  47262  hoidmvle  47297  ovnsubadd2lem  47342  smflimlem6  47473  mbfpsssmf  47480  smfmullem4  47491  smfpimbor1lem1  47495  sqrtnzqaa  47588  nthrucw  47590  goldratmolem2  47606  cjnpoly  47609  sinnpoly  47611  astbstanbst  47629  aistbistaandb  47630  abnotataxb  47636  aifftbifffaibif  47641  confun4  47662  plcofph  47664  plvcofph  47666  plvcofphax  47667  plvofpos  47668  mdandyv0  47669  mdandyv1  47670  mdandyv2  47671  mdandyv3  47672  mdandyv4  47673  mdandyv5  47674  mdandyv6  47675  mdandyv7  47676  mdandyv8  47677  mdandyv9  47678  mdandyv10  47679  mdandyv11  47680  mdandyv12  47681  mdandyv13  47682  mdandyv14  47683  mdandyv15  47684  mdandyvr0  47685  mdandyvr1  47686  mdandyvr2  47687  mdandyvr3  47688  mdandyvr4  47689  mdandyvr5  47690  mdandyvr6  47691  mdandyvr7  47692  mdandyvrx0  47701  mdandyvrx1  47702  mdandyvrx2  47703  mdandyvrx3  47704  mdandyvrx4  47705  mdandyvrx5  47706  mdandyvrx6  47707  mdandyvrx7  47708  dandysum2p2e4  47718  or2expropbilem1  47752  dfnelbr2  47993  2ltceilhalf  48052  flmrecm1  48063  ich2exprop  48203  paireqne  48243  fmtno4prmfac  48307  31prm  48332  lighneallem4a  48343  41prothprmlem2  48353  ppivalnn4  48362  zofldiv2ALTV  48410  nfermltl8rev  48490  nfermltl2rev  48491  nfermltlrev  48492  gbegt5  48509  gbowgt5  48510  gboge9  48512  9gbo  48522  11gbo  48523  nnsum3primes4  48536  nnsum3primesgbe  48540  nnsum4primesodd  48544  nnsum4primesoddALTV  48545  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  tgblthelfgott  48563  tgoldbach  48565  ushggricedg  48675  isubgrgrim  48677  stgrvtx  48702  stgriedg  48703  stgrusgra  48707  stgr1  48709  uspgrlim  48740  grlimprclnbgrvtx  48747  clnbgr3stgrgrlic  48768  usgrexmpl1lem  48769  usgrexmpl2lem  48774  usgrexmpl2nb0  48779  usgrexmpl2nb1  48780  usgrexmpl2nb2  48781  usgrexmpl2nb3  48782  usgrexmpl2nb4  48783  usgrexmpl2nb5  48784  gpgvtx  48791  gpgiedg  48792  gpgorder  48807  gpgvtxedg0  48811  gpgvtxedg1  48812  gpgedgiov  48813  gpg5nbgrvtx03starlem1  48816  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx13starlem1  48819  gpg5nbgrvtx13starlem2  48820  gpg5nbgrvtx13starlem3  48821  gpg3kgrtriexlem3  48833  gpg3kgrtriexlem6  48836  gpgprismgr4cycllem2  48844  gpgprismgr4cyclex  48855  pgnioedg1  48856  pgnioedg2  48857  pgnioedg3  48858  pgnioedg4  48859  pgnioedg5  48860  pgnbgreunbgrlem2lem1  48862  pgnbgreunbgrlem2lem2  48863  pgnbgreunbgrlem2lem3  48864  pgnbgreunbgrlem3  48866  pgnbgreunbgrlem4  48867  pgnbgreunbgrlem5lem1  48868  pgnbgreunbgrlem5lem2  48869  pgnbgreunbgrlem5lem3  48870  pgnbgreunbgrlem6  48872  gpg5ngric  48876  gpg5edgnedg  48878  nn0mnd  48927  mgmplusgiopALT  48942  sgrp2sgrp  48976  2zrngaabl  48998  funcringcsetcALTV2lem8  49045  funcringcsetclem8ALTV  49068  zlmodzxzlmod  49117  zlmodzxzel  49118  zlmodzxzscm  49120  zlmodzxzadd  49121  snlindsntorlem  49233  ldepspr  49236  lmod1lem2  49251  lmod1lem3  49252  lmod1lem4  49253  lmod1lem5  49254  lmodn0  49258  zlmodzxznm  49260  zlmodzxzldeplem  49261  zlmodzxzldeplem1  49263  zlmodzxzldeplem3  49265  lvecpsslmod  49270  ldepsnlinc  49271  ldepslinc  49272  expnegico01  49281  zofldiv2  49294  flnn0div2ge  49296  elbigo2  49315  nnlog2ge0lt1  49329  digfval  49360  dignnld  49366  dignn0flhalf  49381  2arymaptfo  49417  itcovalt2lem1  49438  prelrrx2  49476  eenglngeehlnmlem2  49501  rrxsphere  49511  line2  49515  line2x  49517  line2y  49518  itsclc0yqsollem2  49526  inlinecirc02plem  49549  sepfsepc  49689  invfn  49791  alimp-surprise  50541  aacllem  50584