Theorem 3pm3.2i 818

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

Syntax hints:   /\ wa 223   /\ w3a 775

This theorem is referenced by:  3jaoi 887  limon 3094  trcl 4645  mul0or 5694  divassz 5745  divdivdiv 5789  divdiv23z 5794  ltdiv23 5894  sqrlem6 6678  sqrlem20 6692  abs1m 6904  faclbnd4lem1 6948  bcpasc2t 6968  climsup 7155  caucvglem2 7158  cvgcmpub 7185  infcvgaux1 7219  expcnvlem5 7231  geolim1i 7238  cvgratlem2ALT 7248  ivthlem5 7285  isupivth 7290  efaddlem12 7349  efaddlem20 7357  ef01tllem2 7384  ef01tllem2OLD 7385  eflt 7406  eflegeot 7416  efm1legeo 7417  efm1legeot 7418  efcnlem1 7419  sin01bndlem1 7467  ruclem33 7542  oprcn 7977  isgrpi 8042  isgrp2i 8076  isvci 8201  isnvi 8232  ip1cnilem2 8374  ip1cnilem3 8375  sspid 8384  lnocoi 8418  nmlno0lem 8453  nmblolbii 8459  blocnilem 8464  phpar 8483  ip0i 8484  ip2i 8487  ipdirilem 8488  ipasslem6 8495  ipasslem7 8496  ipasslem8 8497  ipasslem10 8499  ip2dii 8504  siilem1 8511  siilem2 8512  siii 8513  sincnlem 8666  pilem2 8672  pilem3 8673  sincos6thpi 8711  efif1lem7 8736  hhsst 9136  hhsssh2 9140  projlem8 9193  fh1 9564  fh2 9565  pjoi0 9663  eigre 9760  adj1o 9818  elunop2t 9938  bra11 10041  mdslle1 10244  mdslle2 10245  mdslj1 10246  mdslj2 10247  mdslmd1lem1 10252  mdslmd2 10257  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem5 10593  rcfpfillem5OLD 10594  1alg 10654  eloi 10659  1ded 10671  dedalg 10676  0alg 10689  0ded 10690  0cat 10691  1cat 10692  catded 10697

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 777

Copyright terms: Public domain