Theorem 3expa 833

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

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

This theorem is referenced by:  mp3an2 904  mp3an3 905  mpd3an3 917  rgen3 1724  mouniss 2890  f1ocnvfv1 3878  f1ocnvfv2 3879  f1ofveu 3882  isotr 3897  isotrALT 3898  tfrlem11 3921  curry1f 4099  oalimcl 4194  oeordsuc 4221  oelim2 4222  nneob 4255  mapenlem1 4489  ltapi 5030  add4t 5338  cnegextlem2 5346  cnegextlem3 5347  2addsubt 5389  mul4t 5420  muladdt 5421  xrlttrt 5553  ltleaddt 5645  divasst 5741  div23t 5742  div12t 5744  divsubdirtOLD 5775  divmuldivt 5780  divadddivt 5784  divdivdivt 5785  divdiv23t 5792  p1let 5817  lemul12ait 5842  lemul12itOLD 5843  lediv1tOLD 5852  lemuldivtOLD 5875  ltdiv23t 5892  lediv23t 5893  nndivt 5959  lbinfm 6048  nnreclt 6072  xrsupsslem 6076  xrinfmsslem 6077  supxrunb1 6089  zbtwnre 6221  fladdzt 6244  qnegclt 6270  qmulclt 6271  qrecclt 6273  qdivclt 6274  qbtwnre 6278  seq1rn 6322  ioo0t 6368  iooint 6372  iooss1 6373  iooss2 6374  ioojoint 6416  uzss 6431  elfz5t 6474  fznn0subt 6498  fzss1t 6503  fzrevralt 6519  recexpt 6595  expsubt 6598  divexpt 6599  expord2t 6604  expmwordit 6606  exple1t 6607  absmaxt 6897  seq1ublem 6911  caure 6927  cauim 6928  facndivt 6943  faclbnd4lem4 6951  faclbnd4 6952  faclbnd5 6953  bccl2t 6971  2sumeq2dv 6994  fsum1ps 7018  fsumsplit 7020  fsumrev2 7030  fsumshftm 7032  fsum2mul 7037  clm3 7079  climaddlem3 7116  climmullem5 7124  climmullem8 7127  climabslem 7148  caucvglem5 7161  cvgcmp3c 7186  isum1p 7206  isumreclt 7210  isummulc1ALT 7213  cvgratlem1 7250  cvgratlem2 7251  cvgratlem5 7254  abspef01tlub 7395  acdc2lem2 7489  acdc5lem2 7492  infpnlem1 7506  infxpdom 7571  infxp 7572  infmap2 7581  tgss2t 7637  basgen2t 7639  2basgent 7641  subtop 7646  elcls2 7705  innei 7736  cnco 7768  cnsscnp 7772  cncnp 7778  cncnp2 7779  ismsi 7801  ismeti 7802  bl2in 7843  blin 7852  blss 7853  ssbl 7855  opni3 7866  metcnp 7887  metcnp2 7888  metcn 7889  cncfmet 7905  bl2ioo 7911  lmnn 7935  lmuni 7951  lmss 7953  lmle 7960  metelcls 7965  metcnp4lem2 7969  metcn4 7971  xplm 7975  iscms2lem4 7992  iscms2lem5 7993  lmcau 7996  grpidinvlem3 8050  isgrp2i 8076  ring2 8149  isvci 8201  va1cnlem 8345  ipval2lem2 8354  ipval2lem5 8360  sspival 8397  sspimsval 8399  nmoub3i 8436  isblo2 8443  0lno 8450  nmo0 8451  blocni 8465  isph 8481  sspph 8515  ipblnfi 8516  minveclem27 8571  shftefif1olem 8741  relogeftb 8765  hvadd4t 8905  hiassdit 8957  ocsh 9156  occllem6 9178  projlem2 9187  projlem25 9210  projlem26 9211  projlem28 9213  pjeqt 9242  chj4t 9458  spansncol 9491  pjspansnt 9500  pjjs 9645  hoadd4t 9710  homco1t 9727  homulasst 9728  hoadddit 9729  hoadddirt 9730  nmopub2tALT 9833  unoplint 9844  counopt 9845  nmfnleub2t 9850  adjvalvalt 9861  hmoplint 9866  bralnfnt 9872  brafnmult 9875  homco2t 9901  lnopm 9925  lnopco 9928  hmopmt 9946  hmopcot 9948  nmophm 9961  lnfncnbdt 9992  cnlnadjlem2 10001  adjlnopt 10019  adjmult 10025  branmfnt 10038  kbass5t 10053  kbass6t 10054  leop2t 10057  leopmulit 10066  pjima 10104  atcvatlem 10312  irredlem2 10318  mdsymlem3 10332  mdsymlem5 10334  sumdmdi 10342  sumdmdlem 10345  cdj3lem2a 10363  cdj3lem2b 10364  cdj3lem3a 10366  cdj3 10368  homeofval 10516  idhme 10522

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