Theorem 3impb 829

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

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

This theorem is referenced by:  3adant1l 852  3adant1r 853  syl3an1 859  3impdi 880  rcla42ev 1881  reuss 2276  wereu 2945  foprrn 4035  fnoprvalrn 4038  odi 4210  ecopoprtrn 4311  ecoprass 4320  ecoprdi 4321  supmaxlem 4588  addasspi 5023  mulasspi 5025  distrpi 5026  ltapq 5076  ltmpq 5077  genpass 5112  distrpr 5132  ltapr 5151  cnegextlem1 5345  subdit 5427  submul2t 5460  subsub2t 5461  pnpcant 5478  xrlttrt 5553  le2tri3 5589  ltaddsubt 5631  leaddsubt 5633  diveq0t 5768  divnegt 5774  divcan5t 5781  lble 6047  uzind3 6207  lenegsqt 6885  faclbnd4lem4 6951  fsummulc2 7034  clm0i 7089  clim2serzt 7134  iserzcmp0 7143  isummulc1ALT 7213  geoisum1c 7245  fsum0diag2 7259  reeftlclt 7380  uncld 7681  ntrss 7688  innei 7736  sncld 7787  blin 7852  ssbl 7855  opni2 7865  cncfmet 7905  bl2ioo 7911  lmss 7953  bcthlem7 8005  bcthlem9 8007  grpinvid1 8072  grpinvid2 8073  abl4 8105  ablnncan 8112  issubg 8116  issubgi 8122  grpsn 8124  ablmul 8131  ghgrpilem4 8136  vcnegsubdi2 8194  nvnpcan 8280  nvmeq0 8284  nvabs 8301  lnocoi 8418  nmorepnf 8431  blo3i 8462  blometi 8463  ipasslem5 8494  spwpr3OLD 8662  spwpr4OLD 8663  spwpr4aOLD 8664  hvmulcant 8939  his5t 8953  his7t 8956  his2sub2t 8959  hhssnv 9134  pjeq2t 9241  homclt 9524  fh1t 9561  fh2t 9562  cm2jt 9563  homco1t 9727  homulasst 9728  hoadddit 9729  hosubsub2t 9738  braaddt 9869  bramult 9870  kbmult 9879  lnopmult 9891  lnopl 9892  lnopaddmul 9897  lnopsubmul 9899  homco2t 9901  lnfnl 9969  lnfnaddmul 9974  kbass2t 10050  mdexch 10262  symggrpi 10406  cayleylem2 10410  ficli 10472  ficliOLD 10473

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