Theorem 3pm3.2i 1335

Description: Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)

Hypotheses

Ref	Expression
3pm3.2i.1	⊢ 𝜑
3pm3.2i.2	⊢ 𝜓
3pm3.2i.3	⊢ 𝜒

Assertion

Ref	Expression
3pm3.2i	⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Proof of Theorem 3pm3.2i

Step	Hyp	Ref	Expression
1		3pm3.2i.1	. . 3 ⊢ 𝜑
2		3pm3.2i.2	. . 3 ⊢ 𝜓
3	1, 2	pm3.2i 473	. 2 ⊢ (𝜑 ∧ 𝜓)
4		3pm3.2i.3	. 2 ⊢ 𝜒
5		df-3an 1085	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
6	3, 4, 5	mpbir2an 709	1 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Syntax hints:   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  mpbir3an  1337  3jaoi  1423  ftp  6922  hartogslem1  9009  cantnflem3  9157  cantnflem4  9158  trcl  9173  ttukeylem7  9940  f13idfv  13371  faclbnd4lem1  13656  4bc2eq6  13692  hashge3el3dif  13847  funcnvs3  14279  wrdl3s3  14329  infcvgaux1i  15215  halfleoddlt  15714  strleun  16594  strle1  16595  slotsbhcdif  16696  estrres  17392  srgbinomlem4  19296  psrass1  20188  psrass23l  20191  psrass23  20193  mplsubrg  20223  mplmon  20247  mplmonmul  20248  mplcoe1  20249  mplbas2  20254  evlslem2  20295  coe1mul2  20440  cnfldfun  20560  xrsnsgrp  20584  zfbas  22507  ust0  22831  utop2nei  22862  isclmi0  23705  iscvsi  23736  plypf1  24805  1cubr  25423  birthdaylem1  25532  divsqrtsumlem  25560  lgslem2  25877  lgsdir2lem2  25905  lgsdir2lem3  25906  addsqn2reu  26020  addsqrexnreu  26021  addsqnreup  26022  axlowdimlem6  26736  usgrexmpldifpr  27043  0grsubgr  27063  upgrewlkle2  27391  usgr2wlkspthlem2  27542  usgr2pthlem  27547  elwspths2spth  27749  wlk2v2e  27939  ntrl2v2e  27940  konigsberglem4  28037  konigsberglem5  28038  ex-dvds  28238  sspid  28505  lnocoi  28537  nmlno0lem  28573  nmblolbii  28579  blocnilem  28584  phpar  28604  ip0i  28605  ip2i  28608  ipdirilem  28609  ipasslem10  28619  ip2dii  28624  siilem1  28631  siilem2  28632  hhssabloilem  29041  hhsst  29046  hhsssh2  29050  fh1i  29401  fh2i  29402  cm2ji  29405  pjoi0i  29498  elunop2  29793  mdslle1i  30097  mdslle2i  30098  mdslj1i  30099  mdslj2i  30100  mdslmd1lem1  30105  mdslmd2i  30110  dp2lt  30565  dpadd3  30592  threehalves  30595  cyc3evpm  30796  xrge0slmod  30921  xrge0iifmhm  31186  cnzh  31215  rezh  31216  dmvlsiga  31392  eulerpartgbij  31634  hgt750lemd  31923  hgt750lem  31926  hgt750lemb  31931  hgt750leme  31933  nolt02o  33203  dnizeq0  33818  cnndvlem1  33880  taupi  34608  poimirlem28  34924  poimirlem31  34927  poimirlem32  34928  asindmre  34981  areacirc  34991  ishlatiN  36495  rabren3dioph  39418  inductionexd  40511  lhe4.4ex1a  40667  stoweidlem13  42305  stoweidlem26  42318  stoweidlem34  42326  stoweid  42355  wallispilem2  42358  fourierdlem62  42460  fourierdlem103  42501  fouriersw  42523  salexct3  42632  salgensscntex  42634  smfmullem4  43076  pldofph  43188  31prm  43767  9fppr8  43909  6gbe  43943  8gbe  43945  9gbo  43946  11gbo  43947  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  nnsum4primeseven  43972  tgblthelfgott  43987  tgoldbach  43989  zlmodzxzldeplem3  44564  zlmodzxzldep  44566  blennnt2  44656  line2  44746  line2x  44748  line2y  44749