Theorem 3pm3.2i 830

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 789	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		3pm3.2i.1	. . 3 |- ph
3		3pm3.2i.2	. . 3 |- ps
4	2, 3	pm3.2i 292	. 2 |- (ph /\ ps)
5		3pm3.2i.3	. 2 |- ch
6	1, 4, 5	mpbir2an 742	1 |- (ph /\ ps /\ ch)

Syntax hints:   /\ wa 230   /\ w3a 787

This theorem is referenced by:  3jaoi 899  limon 3151  trcl 4707  mul0ori 5759  divasszi 5808  divdivdivi 5847  divdiv23zi 5852  ltdiv23i 5954  sqrlem6 6768  sqrlem20 6782  abs1mi 6994  faclbnd4lem1 7038  bcpasc2 7058  climsupi 7245  caucvglem2 7248  cvgcmpubi 7275  infcvgaux1i 7309  expcnvlem5 7321  geolim1i 7328  cvgratlem2ALT 7338  ivthlem5 7375  isupivthi 7380  efaddlem12 7439  efaddlem20 7447  ef01tllem2 7474  ef01tllem2OLD 7475  eflti 7497  eflegeo 7507  efm1legeoi 7508  efm1legeo 7509  efcnlem1 7510  sin01bndlem1 7559  ruclem33 7634  oprcn 8062  isgrpi 8127  isgrp2i 8160  isvci 8285  isnvi 8316  ip1cnilem2 8458  ip1cnilem3 8459  sspid 8468  lnocoi 8502  nmlno0lem 8537  nmblolbii 8543  blocnilem 8548  phpar 8567  ip0i 8568  ip2i 8571  ipdirilem 8572  ipasslem6 8579  ipasslem7 8580  ipasslem8 8581  ipasslem10 8583  ip2dii 8588  siilem1 8595  siilem2 8596  siii 8597  sincnlem 8749  pilem2 8755  pilem3 8756  sincos6thpi 8794  efif1lem7 8819  hhsst 9219  hhsssh2 9223  projlem8 9276  fh1i 9647  fh2i 9648  pjoi0i 9746  eigrei 9843  adj1o 9901  elunop2 10021  bra11 10124  mdslle1i 10328  mdslle2i 10329  mdslj1i 10330  mdslj2i 10331  mdslmd1lem1 10336  mdslmd2i 10341  inposet 10578  empos 10579  rcfpfillem3 10673  rcfpfillem5 10675  1alg 10736  eloi 10741  1ded 10753  dedalg 10758  0alg 10771  0ded 10772  0cat 10773  1cat 10774  catded 10779

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 154  df-an 232  df-3an 789

Copyright terms: Public domain