Theorem 3expb 832

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

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

This theorem is referenced by:  3adant3r1 840  3adant3r2 841  3adant3r3 842  3adant1l 850  3adant1r 851  syl3an1 857  mp3an1 900  csbiegf 2021  fnfco 3627  oaass 4179  omlimcl 4193  odi 4194  nnmsucr 4224  mapenlem1 4469  add4t 5310  2addsubt 5361  mul4t 5392  subadd4t 5447  ltleaddt 5619  divcan5t 5737  divcan6t 5747  letrp1t 5772  lemul12ait 5798  ltdiv2t 5835  ledivdivt 5838  lediv2t 5839  nndivtrt 5907  sup2 5998  xrinfmsslem 6024  nn0addge1t 6077  nn0addge2t 6078  zltp1let 6128  peano2uz2 6149  uzind 6153  uzind3 6155  flget 6178  qret 6197  qnegclt 6208  qbtwnre 6216  rpdivclt 6229  2shft 6289  uzind4 6382  fzaddelt 6432  fzss2t 6436  fzrevt 6443  divexpt 6530  fsumdivc 6973  fsumdivcALT 6974  clm4le 7019  2climnn 7039  2climnn0 7040  climaddlem3 7052  climmullem1 7056  climmullem5 7060  climmullem8 7063  iserzext 7071  climcmplem 7073  climsqueeze 7076  climsqueeze2 7077  climsup 7091  caucvglem6 7098  mulc1cncf 7214  divccncf 7215  acdc2lem1 7430  acdc5lem1 7433  topbast 7569  basgen2t 7581  uncld 7623  ntrss 7630  elcls3 7652  neissex 7679  mettri3OLD 7759  blin 7792  ssbl 7795  opnin 7809  metcnp 7826  metcnpi3 7831  metcnpi4 7832  metcni2 7834  blssioo 7852  tgioolem 7853  iscau3 7876  lmss 7888  xpcn 7910  lmcau 7930  grpidinvlem2 7983  grpidinvlem3 7984  grpnpncan 8029  abl4 8041  ablmuldiv 8044  ghgrpilem4 8073  ghgrpi 8074  nvaddsub4 8221  nvmeq0 8224  nvcni 8266  sspmval 8326  sspival 8331  sspimsval 8333  lnosub 8353  lnomul 8354  nvcnpi4 8355  0lno 8382  blocnilem 8395  ipsubdir 8439  sspph 8446  ubthlem12 8471  efifolem5 8641  hvadd4t 8826  hvpncant 8829  hiassdit 8878  shscl 9196  shmods 9277  chj4t 9373  spansncol 9407  spanunsn 9419  hoadd4t 9627  hosubadd4t 9657  lnoplt 9754  unopf1ot 9756  counopt 9761  lnfnlt 9771  hmopadj2t 9781  kbmult 9795  eighmret 9803  lnopm 9840  lnophs 9841  hmopst 9860  hmopmt 9861  nmcopexlem6 9871  nmcfnexlem6 9900  cnlnadjlem2 9916  adjmult 9939  adjaddt 9940  kbass6t 9966  mdslj1 10154  mdslj2 10155  mdslmd1lem1 10160  mdslmd2 10165  irredlem3 10227  ghomf1olem 10301  fipfil 10438

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