Theorem 3expb 834

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 832	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp32 363	1 |- ((ph /\ (ps /\ ch)) -> th)

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

This theorem is referenced by:  3adant3r1 842  3adant3r2 843  3adant3r3 844  3adant1l 852  3adant1r 853  syl3an1 859  mp3an1 903  csbiegf 2031  fnfco 3642  oaass 4195  omlimcl 4209  odi 4210  nnmsucr 4240  mapenlem1 4489  add4t 5338  2addsubt 5389  mul4t 5420  subadd4t 5475  ltleaddt 5645  divcan5t 5781  divcan6t 5791  letrp1t 5816  lemul12ait 5842  lediv1t 5851  lemuldivt 5874  ltdiv2t 5887  ledivdivt 5890  lediv2t 5891  nndivtrt 5960  sup2 6051  xrinfmsslem 6077  nn0addge1t 6130  nn0addge2t 6131  zltp1let 6181  peano2uz2 6201  uzind 6205  uzind3 6207  flget 6233  qret 6259  qnegclt 6270  qbtwnre 6278  rpdivclt 6292  2shft 6352  uzind4 6450  fzaddelt 6500  fzss2t 6504  fzrevt 6511  divexpt 6599  fsumdivc 7035  fsumdivcALT 7036  clm4le 7081  2climnn 7102  2climnn0 7103  climaddlem3 7116  climmullem1 7120  climmullem5 7124  climmullem8 7127  iserzext 7135  climcmplem 7137  climsqueeze 7140  climsqueeze2 7141  climsup 7155  caucvglem6 7162  mulc1cncf 7279  divccncf 7280  acdc2lem1 7488  acdc5lem1 7491  topbast 7627  basgen2t 7639  uncld 7681  ntrss 7688  elcls3 7711  neissex 7738  blin 7852  ssbl 7855  opnin 7869  metcnp 7887  metcnpi3 7892  metcnpi4 7893  metcni2 7895  blssioo 7913  tgioolem 7914  iscau3 7938  iscau4 7940  lmss 7953  xpcn 7976  lmcau 7996  grpidinvlem2 8049  grpidinvlem3 8050  grpnpncan 8094  abl4 8105  ablmuldiv 8107  ghgrpilem4 8136  ghgrpi 8137  nvaddsub4 8281  nvmeq0 8284  nvcni 8329  nvcni2 8330  nvcni3 8331  sspmval 8392  sspival 8397  sspimsval 8399  lnosub 8420  lnomul 8421  nvcnpi3 8422  nvcnpi4 8423  0lno 8450  blocnilem 8464  ipsubdir 8508  sspph 8515  ubthlem12 8540  spwpr3OLD 8662  efifolem5 8726  hvadd4t 8905  hvpncant 8908  hiassdit 8957  shscl 9281  shmods 9362  chj4t 9458  spansncol 9491  spanunsn 9502  hoadd4t 9710  hosubadd4t 9740  lnoplt 9838  unopf1ot 9840  counopt 9845  lnfnlt 9855  hmopadj2t 9865  kbmult 9879  eighmret 9887  lnopm 9925  lnophs 9926  hmopst 9945  hmopmt 9946  nmcopexlem6 9956  nmcfnexlem6 9985  cnlnadjlem2 10001  adjmult 10025  adjaddt 10026  kbass6t 10054  mdslj1 10246  mdslj2 10247  mdslmd1lem1 10252  mdslmd2 10257  irredlem3 10319  ghomf1olem 10396  fipfil 10563

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