Theorem pm3.2i 234

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

Syntax hints:   ∧ wa 196

This theorem is referenced by:  pm3.2ni 440  3pm3.2i 603  bm1.3ii 1481  eqssi 1517  unssi 1633  ssini 1660  itlso 2151  we0 2196  ordon 2238  ord0 2276  elvv 2464  relsn 2485  relopab 2494  cnvun 2642  funsn 2690  funi 2692  fnresi 2737  fn0 2739  f0 2772  fconst 2774  f10 2822  f1o0 2824  f1oi 2825  f1osn 2827  fvi 2900  isoid 2933  tfrlem7 2955  tfr1 2962  tz7.44-1 2966  tz7.44-2 2967  frfnom 2989  fnoprab 3038  fo1st 3094  fo2nd 3095  1st2val 3097  df1st2 3098  ster 3207  th3q 3253  fnmap 3262  mapvalg 3263  2dom 3332  endisj 3341  canth2 3381  xpmapenlem1 3391  xpmapenlem5 3395  limensuci 3401  phplem3 3405  unfilem2 3439  unfi 3441  en2lp 3453  opthreg 3455  rankpw 3528  rankuni 3533  aceq6b 3565  zorn2 3612  alephiso 3697  cflecard 3707  cdavalt 3716  uncdadom 3718  cdaen 3719  cda1en 3721  cdacomen 3724  cdaassen 3725  xpcdaen 3726  1pi 3805  mulidpq 3863  1lt2pq 3872  1pr 3911  prlem934a 3931  m1p1sr 3995  m1m1sr 3996  0idsr 4000  1idsr 4001  00sr 4002  recexsrlem 4006  addresr 4050  mulresr 4051  ax0id 4076  ax1id 4077  axi2m1 4082  axcnre 4087  negeu 4124  add4 4130  mul4 4180  muln0 4214  receu 4215  divval 4217  divneq0 4231  dividt 4256  recrect 4260  divmuldiv 4266  divadddiv 4268  divdivdiv 4269  recdivt 4270  nnind 4434  nnleltp1t 4448  0z 4573  om2uzuz 4653  om2uzf1o 4656  uzrdgval 4657  uzrdgini 4658  seqval 4665  sqr0 4730  sqrlem6 4736  sqrlem8 4738  sqrlem23 4753  nthruc 4784  nthruz 4785  clim0 4882  climunii 4883  climuni 4884  ruclem10 4894  ruclem11 4895  ruclem13 4897  ruclem35 4919  ruc 4924  qnnen 4931  hvadd4 5030  normlem7t 5072  norm3adif 5095  hlim0 5140  hlimcaui 5141  hlimunii 5143  hlimuni 5144  helch 5151  hsn0elch 5155  occl 5188  projlem7 5199  projlem8 5200  omls 5251  pjpj0 5259  shscl 5282  shintcl 5294  shintclt 5295  chintcl 5296  chintclt 5297  shincl 5332  shsumval2 5361  chincl 5382  chabs1t 5432  osumlem7 5536  pjcomp 5565  pjf 5588  hoscl 5596  hodcl 5597  hoco 5598  hoscom 5605  hods 5606  hosass 5607  hosdir 5609  hoddir 5610  ho0 5612  ho1 5613  hoid0 5614  pjsdi 5625  pjddi 5626  pjscj 5640  pjtot 5644  pjnorm 5663  sto1 5677  stle 5681  stji1 5683

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org