Theorem 3pm3.2i 817

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 776	. 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 729	1 |- (ph /\ ps /\ ch)

Syntax hints:   /\ wa 223   /\ w3a 774

This theorem is referenced by:  3jaoi 886  limon 3090  trcl 4628  mul0or 5673  divassz 5718  divdivdiv 5755  divdiv23z 5760  ltdiv23 5852  sqrlem6 6623  sqrlem20 6637  abs1m 6856  faclbnd4lem1 6900  bcpasc2t 6921  climsup 7108  caucvglem2 7111  cvgcmpub 7138  infcvgaux1 7171  expcnvlem5 7183  geolim1i 7190  cvgratlem2ALT 7200  ivthlem5 7237  isupivth 7242  ivthlem4OLD 7245  ivthlem5OLD 7246  ivth2OLD 7251  efaddlem12 7308  efaddlem20 7316  ef01tllem2 7343  eflt 7364  eflegeot 7373  efm1legeo 7374  efm1legeot 7375  efcnlem1 7376  reeff1olem1OLD 7383  sin01bndlem1 7426  ruclem33 7502  oprcn 7939  isgrpi 8004  isgrp2i 8038  isvci 8165  isnvi 8196  ip1cnilem2 8336  ip1cnilem3 8337  sspid 8346  lnocoi 8380  nmlno0lem 8413  nmblolbii 8418  blocnilem 8423  phpar 8442  ip0i 8443  ip2i 8446  ipdirilem 8447  ipasslem6 8454  ipasslem7 8455  ipasslem8 8456  ipasslem10 8458  ip2dii 8463  siilem1 8470  siilem2 8471  siii 8472  sincnlem 8620  pilem2 8626  pilem3 8627  sincos6thpi 8663  efif1lem7 8686  hhsst 9091  hhsssh2 9095  projlem8 9148  fh1 9521  fh2 9522  pjoi0 9620  eigre 9717  adj1o 9775  elunop2t 9894  bra11 9997  mdslle1 10200  mdslle2 10201  mdslj1 10202  mdslj2 10203  mdslmd1lem1 10208  mdslmd2 10213  rcfpfillem3 10513  rcfpfillem5 10515  1alg 10570  eloi 10575  1ded 10587  dedalg 10592  0alg 10605  0ded 10606  0cat 10607  1cat 10608  catded 10613

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 776

Copyright terms: Public domain