Theorem 3impb 828

Description: Importation from double to triple conjunction.

Hypothesis

Ref	Expression
3impb.1	|- ((ph /\ (ps /\ ch)) -> th)

Assertion

Ref	Expression
3impb	|- ((ph /\ ps /\ ch) -> th)

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	exp32 377	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 826	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 774

This theorem is referenced by:  3adant1l 851  3adant1r 852  syl3an1 858  3impdi 878  rcla42ev 1877  reuss 2272  wereu 2940  foprrn 4026  fnoprvalrn 4029  odi 4200  ecopoprtrn 4301  ecoprass 4310  ecoprdi 4311  supmaxlem 4568  addasspi 5003  mulasspi 5005  distrpi 5006  ltapq 5056  ltmpq 5057  genpass 5092  distrpr 5112  ltapr 5131  cnegextlem1 5325  subdit 5407  submul2t 5440  subsub2t 5441  pnpcant 5458  xrlttrt 5534  le2tri3 5571  ltaddsubt 5613  leaddsubt 5615  diveq0t 5732  divnegt 5738  divcan5t 5745  lble 6002  uzind3 6163  lenegsqt 6831  faclbnd4lem4 6896  fsummulc2 6980  clm0i 7035  clim2serzt 7078  iserzcmp0 7087  isummulc1ALT 7156  geoisum1c 7188  fsum0diag2 7202  reeftlclt 7330  uncld 7631  ntrss 7638  innei 7686  sncld 7737  blin 7804  ssbl 7807  opni2 7817  cncfmet 7857  bl2ioo 7863  lmss 7904  bcthlem7 7955  bcthlem9 7957  grpinvid1 8022  grpinvid2 8023  abl4 8056  ablnncan 8064  issubg 8068  issubgi 8074  grpsn 8076  ablmul 8083  ghgrpilem4 8088  vcnegsubdi2 8146  nvnpcan 8232  nvmeq0 8236  nvabs 8253  lnocoi 8365  nmorepnf 8376  blo3i 8406  blometi 8407  ipasslem5 8438  circgrpOLD 8677  hvmulcant 8878  his5t 8892  his7t 8895  his2sub2t 8898  hhssnv 9073  pjeq2t 9179  homclt 9464  fh1t 9501  fh2t 9502  cm2jt 9503  homco1t 9667  homulasst 9668  hoadddit 9669  hosubsub2t 9678  braaddt 9808  bramult 9809  kbmult 9818  lnopmult 9830  lnopl 9831  lnopaddmul 9836  lnopsubmul 9838  homco2t 9840  lnfnl 9907  lnfnaddmul 9912  kbass2t 9988  mdexch 10199  symggrpi 10340  cayleylem2 10344  ficli 10404

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