Theorem 3impb 841

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 386	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 839	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787

This theorem is referenced by:  3adant1l 864  3adant1r 865  syl3an1 871  3impdi 892  rcla42ev 1928  reuss 2327  wereu 3002  foprrn 4093  fnoprvalrn 4096  odi 4268  ecopoprtrn 4372  ecoprass 4381  ecoprdi 4382  supmaxlem 4648  addasspi 5088  mulasspi 5090  distrpi 5091  ltapq 5141  ltmpq 5142  genpass 5177  distrpr 5197  ltapr 5216  cnegexlem1 5410  subdi 5492  submul2 5525  subsub2 5526  pnpcan 5543  xrlttr 5618  le2tri3i 5654  ltaddsub 5696  leaddsub 5698  diveq0 5825  divneg 5831  divcan5 5839  lble 6129  uzind3 6292  qdivcl 6326  irrmul 6330  modcyc 6376  modcycOLD 6377  modcyc2 6378  modcyc2OLD 6379  lenegsq 6975  faclbnd4lem4 7041  fsummulc2 7124  clm0ii 7179  clim2serz 7224  iserzcmp0 7233  isummulc1iALT 7303  geoisum1c 7335  fsum0diag2 7349  reeftlcl 7470  uncld 7766  ntrss 7773  innei 7821  sncld 7872  blin 7937  ssbl 7940  opni2 7950  cncfmet 7990  bl2ioo 7996  lmss 8038  bcthlem7 8090  bcthlem9 8092  grpinvid1 8156  grpinvid2 8157  abl4 8189  ablnncan 8196  issubg 8200  issubgi 8206  grpsn 8208  ablmul 8215  ghgrpilem4 8220  vcnegsubdi2 8278  nvnpcan 8364  nvmeq0 8368  nvabs 8385  lnocoi 8502  nmorepnf 8515  blo3i 8546  blometi 8547  ipasslem5 8578  spwpr4OLD 8746  spwpr4aOLD 8747  hvmulcan 9022  his5 9036  his7 9039  his2sub2 9042  hhssnv 9217  pjeq2 9324  homcl 9607  fh1 9644  fh2 9645  cm2j 9646  homco1 9810  homulass 9811  hoadddi 9812  hosubsub2 9821  braadd 9952  bramul 9953  kbmul 9962  lnopmul 9974  lnopli 9975  lnopaddmuli 9980  lnopsubmuli 9982  homco2 9984  lnfnli 10052  lnfnaddmuli 10057  kbass2 10133  mdexchi 10346  symggrpi 10491  cayleylem2 10495  ficli 10553

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