Theorem 3pm3.2i 1048

Description: Infer conjunction of premises.

Hypotheses

Ref	Expression
3pm3.2i.1	|- ph
3pm3.2i.2	|- ps
3pm3.2i.3	|- ch

Assertion

Ref	Expression
3pm3.2i	|- (ph /\ ps /\ ch)

Proof of Theorem 3pm3.2i

Step	Hyp	Ref	Expression
1		df-3an 860	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		3pm3.2i.1	. . 3 |- ph
3		3pm3.2i.2	. . 3 |- ps
4	2, 3	pm3.2i 307	. 2 |- (ph /\ ps)
5		3pm3.2i.3	. 2 |- ch
6	1, 4, 5	mpbir2an 800	1 |- (ph /\ ps /\ ch)

Syntax hints:   /\ wa 240   /\ w3a 858

This theorem is referenced by:  mpbir3an 1052  3jaoi 1160  trcl 5752  sqrlem6 7928  sqrlem20 7942  faclbnd4lem1 8200  bcpasc2 8220  climsupi 8415  caucvglem2 8418  cvgcmpubi 8446  infcvgaux1i 8480  expcnvlem5 8492  cvgratlem2ALT 8510  isupivthi 8552  efaddlem12 8611  efaddlem20 8619  ef01tllem2 8646  ef01tllem2OLD 8647  eflti 8671  eflegeo 8681  efm1legeo 8683  efcnlem1 8684  sin01bndlem1 8733  ruclem33 8811  oprcn 9255  ip1cnilem2 9713  ip1cnilem3 9714  sspid 9723  lnocoi 9757  nmlno0lem 9793  nmblolbii 9799  blocnilem 9804  phpar 9824  ip0i 9825  ip2i 9828  ipdirilem 9829  ipasslem6 9836  ipasslem7 9837  ipasslem8 9838  ipasslem10 9840  ip2dii 9845  siilem1 9852  siilem2 9853  sincnlem 10015  pilem2 10021  pilem3 10022  sincos6thpi 10061  efif1lem7 10090  hhsst 10769  hhsssh2 10773  projlem8 10826  fh1i 11197  fh2i 11198  cm2ji 11201  pjoi0i 11298  elunop2 11575  mdslle1i 11889  mdslle2i 11890  mdslj1i 11891  mdslj2i 11892  mdslmd1lem1 11897  mdslmd2i 11902  eloi 14400  inposet 14620  dispos 14632  rcfpfillem3 14930  rcfpfillem5 14932  cntrsetlem 14999  lteqtpos 15024  1alg 15069  1ded 15085  dedalg 15090  0alg 15103  0ded 15104  0cat 15105  1cat 15106  catded 15111  dualalg 15131  catsbc 15197  fsumleisumi 15826  trirn 15834  piececn 15894  cncfres 15895  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  heiborlem33 15987  bfplem7 16004  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  reparphtlem2 16064  pcocn 16076  pcohtpylem3 16082  pcopt 16084  pcoass 16085  pcorevlem 16086  isopi 16910  ishlati 17019

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 164  df-an 242  df-3an 860

Copyright terms: Public domain