Theorem 3impb 827

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 825	1 |- ((ph /\ ps /\ ch) -> th)

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

This theorem is referenced by:  3adant1l 850  3adant1r 851  syl3an1 857  3impdi 877  rcla42ev 1872  reuss 2266  wereu 2935  foprrn 4020  fnoprvalrn 4023  odi 4194  ecopoprtrn 4295  ecoprass 4304  ecoprdi 4305  addasspi 4995  mulasspi 4997  distrpi 4998  ltapq 5048  ltmpq 5049  genpass 5084  distrpr 5104  ltapr 5123  cnegextlem1 5317  subdit 5399  submul2t 5432  subsub2t 5433  pnpcant 5450  xrlttrt 5526  le2tri3 5563  ltaddsubt 5605  leaddsubt 5607  diveq0t 5724  divnegt 5730  divcan5t 5737  lble 5994  uzind3 6155  lenegsqt 6823  faclbnd4lem4 6888  fsummulc2 6972  clm0i 7027  clim2serzt 7070  iserzcmp0 7079  isummulc1ALT 7148  geoisum1c 7180  fsum0diag2 7194  reeftlclt 7322  uncld 7623  ntrss 7630  innei 7677  sncld 7726  blin 7792  ssbl 7795  opni2 7805  cncfmet 7844  bl2ioo 7850  lmss 7888  bcthlem7 7939  bcthlem9 7941  grpinvid1 8006  grpinvid2 8007  abl4 8041  ablnncan 8049  issubg 8053  issubgi 8059  grpsn 8061  ablmul 8068  ghgrpilem4 8073  vcnegsubdi2 8131  nvnpcan 8220  nvmeq0 8224  nvabs 8240  lnocoi 8352  nmorepnf 8363  blo3i 8393  blometi 8394  ipasslem5 8425  circgrpOLD 8658  hvmulcant 8860  his5t 8874  his7t 8877  his2sub2t 8880  hhssnv 9054  pjeq2t 9156  homclt 9441  fh1t 9478  fh2t 9479  cm2jt 9480  homco1t 9644  homulasst 9645  hoadddit 9646  hosubsub2t 9655  braaddt 9785  bramult 9786  kbmult 9795  lnopmult 9807  lnopl 9808  lnopaddmul 9813  lnopsubmul 9815  homco2t 9817  lnfnl 9884  lnfnaddmul 9889  kbass2t 9962  mdexch 10170  symggrpiOLD 10311  symggrpi 10313  cayleylem2 10317  ficli 10368

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