Theorem 3expb 833

Description: Exportation from triple to double conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3expb

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 831	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp32 363	1 |- ((ph /\ (ps /\ ch)) -> th)

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

This theorem is referenced by:  3adant3r1 841  3adant3r2 842  3adant3r3 843  3adant1l 851  3adant1r 852  syl3an1 858  mp3an1 901  csbiegf 2027  fnfco 3633  oaass 4185  omlimcl 4199  odi 4200  nnmsucr 4230  mapenlem1 4475  add4t 5318  2addsubt 5369  mul4t 5400  subadd4t 5455  ltleaddt 5627  divcan5t 5745  divcan6t 5755  letrp1t 5780  lemul12ait 5806  ltdiv2t 5843  ledivdivt 5846  lediv2t 5847  nndivtrt 5915  sup2 6006  xrinfmsslem 6032  nn0addge1t 6085  nn0addge2t 6086  zltp1let 6136  peano2uz2 6157  uzind 6161  uzind3 6163  flget 6186  qret 6205  qnegclt 6216  qbtwnre 6224  rpdivclt 6237  2shft 6297  uzind4 6390  fzaddelt 6440  fzss2t 6444  fzrevt 6451  divexpt 6538  fsumdivc 6981  fsumdivcALT 6982  clm4le 7027  2climnn 7047  2climnn0 7048  climaddlem3 7060  climmullem1 7064  climmullem5 7068  climmullem8 7071  iserzext 7079  climcmplem 7081  climsqueeze 7084  climsqueeze2 7085  climsup 7099  caucvglem6 7106  mulc1cncf 7222  divccncf 7223  acdc2lem1 7438  acdc5lem1 7441  topbast 7577  basgen2t 7589  uncld 7631  ntrss 7638  elcls3 7661  neissex 7688  mettri3OLD 7770  blin 7804  ssbl 7807  opnin 7821  metcnp 7839  metcnpi3 7844  metcnpi4 7845  metcni2 7847  blssioo 7865  tgioolem 7866  iscau3 7890  iscau4 7892  lmss 7904  xpcn 7926  lmcau 7946  grpidinvlem2 7999  grpidinvlem3 8000  grpnpncan 8044  abl4 8056  ablmuldiv 8059  ghgrpilem4 8088  ghgrpi 8089  nvaddsub4 8233  nvmeq0 8236  nvcni 8279  sspmval 8339  sspival 8344  sspimsval 8346  lnosub 8366  lnomul 8367  nvcnpi4 8368  0lno 8395  blocnilem 8408  ipsubdir 8452  sspph 8459  ubthlem12 8484  efifolem5 8660  hvadd4t 8844  hvpncant 8847  hiassdit 8896  shscl 9219  shmods 9300  chj4t 9396  spansncol 9430  spanunsn 9442  hoadd4t 9650  hosubadd4t 9680  lnoplt 9777  unopf1ot 9779  counopt 9784  lnfnlt 9794  hmopadj2t 9804  kbmult 9818  eighmret 9826  lnopm 9863  lnophs 9864  hmopst 9883  hmopmt 9884  nmcopexlem6 9894  nmcfnexlem6 9923  cnlnadjlem2 9939  adjmult 9963  adjaddt 9964  kbass6t 9992  mdslj1 10183  mdslj2 10184  mdslmd1lem1 10189  mdslmd2 10194  irredlem3 10256  ghomf1olem 10330  fipfil 10474

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