Theorem pm3.2i 285

Description: Infer conjunction of premises.

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 283	. 2 ⊢ (φ → (ψ → (φ ⋀ ψ)))
4	1, 2, 3	mp2 43	1 ⊢ (φ ⋀ ψ)

Syntax hints:   ⋀ wa 223

This theorem is referenced by:  pm4.87 356  dfbi 518  pm3.2ni 583  3pm3.2i 822  unssi 2214  ssini 2242  bm1.3ii 2719  elvv 3242  relopab 3280  oprabval5 4043  1st2val 4109  2nd2val 4110  elxp7 4117  df1st2 4140  df2nd2 4141  ster 4282  th3q 4331  fnmap 4343  mapvalg 4344  pmvalg 4345  2dom 4441  endisj 4452  xpmapenlem1 4511  limensuci 4521  phplem2 4524  unfi 4564  abfii4 4574  en2lp 4614  aceq6b 4754  zorn 4809  cflecard 4925  cdavalt 4932  uncdadom 4934  cdaen 4937  cda1en 4939  cdaassen 4943  xpcdaen 4944  mulidpq 5082  1lt2pq 5091  1pr 5130  prlem934a 5150  m1p1sr 5214  m1m1sr 5215  0idsr 5219  1idsr 5220  00sr 5221  recexsrlem 5225  addresr 5269  mulresr 5270  ltsor 5274  ax0id 5294  ax1id 5295  axi2m1 5298  axcnre 5299  add4 5355  mul4 5438  muladd 5439  addsub4 5487  renfdisj 5552  recextlem1 5695  muln0 5712  div11t 5768  recrect 5780  divmuldiv 5790  divadddiv 5792  divdivdiv 5793  recdivt 5794  lemulge11t 5852  reclt1t 5904  dfnn2 5942  nnleltp1t 5960  halfpm6th 6038  2halvest 6045  halfaddsubt 6047  nominpos 6049  xrsupsslem 6082  xrinfmsslem 6083  xrsup0 6103  nneo 6206  zneo 6209  dfuz 6211  seqzres 6573  seqzres2 6574  dfseq0 6576  sqr0 6686  sqrlem6 6692  sqrlem8 6694  sqr2gt1lt2 6733  crrecz 6755  nthruc 6759  nthruz 6760  recjt 6832  faclbnd2 6960  faclbnd4lem1 6962  climuni 7113  climaddlem3 7130  climaddc 7146  climmulc 7147  caucvg3a 7178  caucvg3lem 7180  caucvg3t 7182  cvgcmpub 7199  cvgcmp3cetlem1 7202  cvgcmp3cetlem2 7203  infcvglem2 7236  expcnvlem2 7242  expcnvlem5 7245  geolimilem 7249  geolim 7251  geolim1 7253  ivthlem1 7295  ivthlem4 7298  ivthlem8 7302  isupivth 7304  dsupivthlem 7305  efcltlem1 7318  efseq1ex 7320  erelem1 7333  erelem3 7335  ege2le3lem2 7343  ef0 7349  efaddlem6 7357  efaddlem10 7361  efaddlem12 7363  efaddlem20 7371  efaddlem22 7373  efaddlem26 7377  efaddlem27 7378  efaddlem28 7379  ef01tllem2 7398  ef01tllem2OLD 7399  absef01tlub 7402  eirrlem2 7404  eirrlem3 7405  eflegeolem2 7428  eflegeot 7430  efm1legeot 7432  efcnlem4 7436  reeff1olem1 7438  reeff1olem2 7439  efivalt 7461  sinadd 7465  cosadd 7466  cos1bnd 7489  cos2bnd 7490  sincos2sgn 7495  ruclem35 7559  isbasis3g 7625  qdensere 7760  blex 7858  opnm 7869  ioo2bl 7921  tgioo 7924  bcthlem1 8008  bcth 8041  ghgrpi 8145  cnring 8170  ringsn 8171  nvz0 8304  ipid 8371  blocni 8473  ipdirilem 8496  ipasslem6 8503  ipasslem7 8504  siilem1 8519  minveclem16 8568  minveclem19 8571  minveclem25 8577  minveclem27 8579  minveclem38 8590  htthlem12 8639  spwval2 8661  sincolem 8672  pilem1 8678  pilem2 8679  sinhalfpilem 8686  sinperlem1 8693  sincos4thpi 8717  sincos6thpi 8718  efifolem1 8729  efifolem5 8733  efifolem7 8735  efif1lem7 8743  hvadd4 8932  normlem7tALT 8992  hlim0 9112  hlimuni 9116  helch 9123  hsn0elch 9127  hhshsslem2 9145  hhsssh 9146  projlem7 9199  omls 9253  shscl 9288  shintcl 9300  shintclt 9301  chintcl 9302  chintclt 9303  shincl 9338  shsumval2 9367  chincl 9390  chabs1t 9446  fh1 9571  fh2 9572  pjnorm 9673  mayete3 9680  dfiop2 9686  nmopsetn0 9799  nmfnsetn0 9812  lnop0t 9897  lnophmt 9951  nmcopexlem2 9959  nmbdfnlbt 9986  nmcfnexlem2 9988  nlelsh 10000  nmoptri 10034  bdophs 10036  bdopco 10038  nmopcoadj 10041  hmopidmch 10086  hmopidmcht 10088  hmopidmpjt 10089  hstle1t 10161  hst0t 10168  sto1 10171  stle 10175  stji1 10177  strlem3a 10187  strlem5 10190  jplem1 10203  csmdsym 10269  irredt 10330  mdcompl 10364  dmdcompl 10365  cayleylem3 10419  cdrci 10500  hmeogrp 10544  clicls 10613  mslb1 10620  msra3 10622  1ded 10662  relrded 10666  0ded 10681  0cat 10682  1cat 10683  relrcat 10687  isfuna 10746  emhgrat 10767

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain