Theorem 3expa 831

Description: Exportation from triple to double conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 830	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 362	1 |- (((ph /\ ps) /\ ch) -> th)

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

This theorem is referenced by:  mp3an2 901  mp3an3 902  mpd3an3 914  rgen3 1716  mouniss 2880  f1ocnvfv1 3863  f1ocnvfv2 3864  f1ofveu 3867  isotr 3882  isotrALT 3883  tfrlem11 3906  curry1f 4083  oalimcl 4178  oeordsuc 4205  oelim2 4206  nneob 4239  mapenlem1 4469  ltapi 5002  add4t 5310  cnegextlem2 5318  cnegextlem3 5319  2addsubt 5361  mul4t 5392  muladdt 5393  xrlttrt 5526  ltleaddt 5619  divasst 5704  div23t 5705  div12t 5707  divsubdirt 5731  divmuldivt 5736  divadddivt 5740  divdivdivt 5741  divdiv23t 5748  p1let 5773  lemul12ait 5798  lemul12itOLD 5799  lediv1t 5806  lemuldivt 5824  ltdiv23t 5840  lediv23t 5841  nndivt 5906  lbinfm 5995  nnreclt 6019  xrsupsslem 6023  xrinfmsslem 6024  supxrunb1 6036  zbtwnre 6169  fladdzt 6187  qnegclt 6208  qmulclt 6209  qrecclt 6211  qdivclt 6212  qbtwnre 6216  seq1rn 6259  ioo0t 6305  iooint 6309  iooss1 6310  iooss2 6311  uzss 6363  elfz5t 6406  fznn0subt 6430  fzss1t 6435  fzrevralt 6451  recexpt 6526  expsubt 6529  divexpt 6530  expord2t 6535  expmwordit 6537  exple1t 6538  seq1ublem 6848  caure 6864  cauim 6865  facndivt 6880  faclbnd4lem4 6888  faclbnd4 6889  faclbnd5 6890  bccl2t 6909  2sumeq2dv 6932  fsum1ps 6956  fsumsplit 6958  fsumrev2 6968  fsumshftm 6970  fsum2mul 6975  clm3 7017  climaddlem3 7052  climmullem5 7060  climmullem8 7063  climabslem 7084  caucvglem5 7097  cvgcmp3c 7122  isum1p 7141  isumreclt 7145  isummulc1ALT 7148  cvgratlem1 7185  cvgratlem2 7186  cvgratlem5 7189  abspef01tlub 7336  acdc2lem2 7431  acdc5lem2 7434  infpnlem1 7449  infxpdom 7514  infxp 7515  infmap2 7523  tgss2t 7579  basgen2t 7581  2basgent 7583  subtop 7588  elcls2 7647  innei 7677  cnco 7707  cnsscnp 7711  cncnp 7717  cncnp2 7718  ismsi 7740  ismeti 7741  mettriOLD 7757  bl2in 7783  blin 7792  blss 7793  ssbl 7795  opni3 7806  metcnp 7826  metcnp2 7827  metcn 7828  cncfmet 7844  bl2ioo 7850  lmnn 7873  lmuni 7886  lmss 7888  lmle 7895  metelcls 7900  metcnp4lem2 7903  metcn4 7905  xplm 7909  iscms2lem4 7926  iscms2lem5 7927  lmcau 7930  grpidinvlem3 7984  isgrp2i 8011  ring2 8086  isvci 8139  va1cnlem 8279  ipval2lem2 8288  ipval2lem5 8294  sspival 8331  sspimsval 8333  nmoub3i 8368  isblo2 8375  0lno 8382  nmo0 8383  blocni 8396  isph 8412  sspph 8446  ipblnfi 8447  minveclem27 8502  shftefif1olem 8661  shftefif1olemOLD 8662  relogeftb 8687  hvadd4t 8826  hiassdit 8878  ocsh 9072  occllem6 9094  projlem2 9103  projlem25 9126  projlem26 9127  projlem28 9129  pjeqt 9157  chj4t 9373  spansncol 9407  pjspansnt 9417  pjjs 9562  hoadd4t 9627  homco1t 9644  homulasst 9645  hoadddit 9646  hoadddirt 9647  nmopub2tALT 9750  unoplint 9760  counopt 9761  nmfnleub2t 9766  adjvalvalt 9777  hmoplint 9782  bralnfnt 9788  brafnmult 9791  homco2t 9817  lnopm 9840  lnopco 9843  hmopmt 9861  hmopcot 9863  nmophm 9876  lnfncnbdt 9907  cnlnadjlem2 9916  adjlnopt 9934  adjmult 9939  branmfnt 9951  kbass5t 9965  kbass6t 9966  leop2t 9969  leopmulit 9978  pjima 10015  atcvatlem 10220  irredlem2 10226  mdsymlem3 10240  mdsymlem5 10242  sumdmdi 10249  sumdmdlem 10252  cdj3lem2a 10268  cdj3lem2b 10269  cdj3lem3a 10271  cdj3 10273  homeofval 10403  idhme 10409

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