Theorem 3pm3.2i 816

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

Syntax hints:   /\ wa 223   /\ w3a 773

This theorem is referenced by:  3jaoi 884  limon 3084  trcl 4617  mul0or 5663  divassz 5708  divdivdiv 5745  divdiv23z 5750  ltdiv23 5842  sqrlem6 6608  sqrlem20 6622  abs1m 6841  faclbnd4lem1 6885  bcpasc2t 6906  climsup 7091  caucvglem2 7094  cvgcmpub 7121  infcvgaux1 7154  expcnvlem5 7166  geolim1i 7173  cvgratlem2ALT 7183  ivthlem5 7220  isupivth 7225  ivthlem4OLD 7228  ivthlem5OLD 7229  ivth2OLD 7234  efaddlem12 7291  efaddlem20 7299  ef01tllem2 7326  eflt 7347  eflegeot 7356  efm1legeo 7357  efm1legeot 7358  efcnlem1 7359  reeff1olem1OLD 7366  sin01bndlem1 7409  ruclem33 7485  oprcn 7911  isgrpi 7976  isgrp2i 8011  isvci 8139  isnvi 8171  isnviOLD 8172  ip1cnilem2 8308  ip1cnilem3 8309  sspid 8318  lnocoi 8352  nmlno0lem 8385  nmblolbii 8390  blocnilem 8395  phpar 8414  ip0i 8415  ip2i 8418  ipdirilem 8419  ipasslem6 8426  ipasslem7 8427  ipasslem8 8428  ipasslem10 8430  ip2dii 8435  siilem1 8442  siilem2 8443  siii 8444  sincnlem 8585  pilem2 8591  pilem3 8592  sincos6thpi 8628  efif1lem7 8651  hhsst 9056  projlem8 9109  fh1 9481  fh2 9482  pjoi0 9580  eigre 9677  adj1o 9735  elunop2t 9853  bra11 9954  mdslle1 10152  mdslle2 10153  mdslj1 10154  mdslj2 10155  mdslmd1lem1 10160  mdslmd2 10165  1alg 10498  eloi 10503  1ded 10515  dedalg 10520  0alg 10533  0ded 10534  0cat 10535  1cat 10536  catded 10541

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  df-3an 775

Copyright terms: Public domain