Theorem 3expb 840

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

Syntax hints:   -> wi 3   /\ wa 221   /\ w3a 781

This theorem is referenced by:  3adant3r1 848  3adant3r2 849  3adant3r3 850  3adant1l 858  3adant1r 859  syl3an1 865  mp3an1 909  csbiegf 2083  fnfco 3749  oaass 4331  omlimcl 4345  odi 4346  nnmsucr 4380  mapenlem1 4636  add4 5492  2addsub 5543  mul4 5574  subadd4 5629  ltleadd 5799  div23 5888  div12 5890  divsubdir 5914  divcan5 5920  divadddiv 5923  divdivdiv 5924  divcan6 5930  divdiv23 5931  letrp1 5956  lemul12b 5986  lediv1 5995  lt2mul2div 6016  lemuldiv 6020  ltdiv2 6032  ledivdiv 6035  lediv2 6036  ltdiv23 6037  lediv23 6038  nndivre 6097  nndivtr 6106  rpdivcl 6208  rerpdivcl 6210  sup2 6219  xrinfmsslem 6245  nn0addge1 6298  nn0addge2 6299  zltp1le 6349  peano2uz2 6372  uzind 6376  uzind3 6378  qre 6398  qnegcl 6409  irrmul 6417  qbtwnre 6418  flge 6431  modlt 6463  flmulnn0 6467  flmulnn0OLD 6468  modcyc 6475  uzind4 6577  fzaddel 6630  fzss2 6634  fzrev 6642  2shfti 6717  expdiv 6796  fsumdivc 7238  fsumdivcALT 7239  clm4lei 7284  2climnn 7305  2climnn0 7306  climaddlem3 7319  climmullem1 7323  climmullem5 7327  climmullem8 7330  iserzex 7338  climcmplem 7340  climsqueeze 7343  climsqueeze2 7344  climsupi 7358  caucvglem6 7365  mulc1cncf 7484  divccncf 7485  acdc2lem1 7700  acdc5lem1 7703  topbas 7839  basgen2 7851  uncld 7891  ntrss 7898  elcls3 7921  neissex 7948  blin 8062  ssbl 8065  opnin 8079  metcnp 8098  metcnpi3 8103  metcnpi4 8104  metcni2 8106  blssioo 8124  tgioolem 8125  iscau3 8149  iscau4 8151  lmss 8164  xpcn 8187  lmcau 8207  grpidinvlem2 8262  grpidinvlem3 8263  grpnpncan 8312  abl4 8346  ablmuldiv 8348  gxdi 8355  ghgrpilem4 8377  ghgrpi 8378  nvaddsub4 8528  nvmeq0 8531  nvcni 8576  nvcni2 8577  nvcni3 8578  sspmval 8646  sspival 8651  sspimsval 8653  lnosub 8674  lnomul 8675  nvcnpi3 8676  nvcnpi4 8677  0lno 8705  blocnilem 8719  ipsubdir 8764  sspph 8771  ubthlem12 8798  ubthlem12OLD 8799  efifolem5 8998  hvadd4 9180  hvpncan 9183  hiassdi 9233  shscli 9557  shmodsi 9638  chj4 9734  spansncol 9767  spanunsni 9778  hoadd4 9990  hosubadd4 10020  lnopl 10118  unopf1o 10120  counop 10125  lnfnl 10135  hmopadj2 10145  kbmul 10159  eighmre 10167  lnopmi 10204  lnophsi 10205  hmops 10224  hmopm 10225  nmcopexlem6 10235  nmcfnexlem6 10264  cnlnadjlem2 10280  adjmul 10304  adjadd 10305  kbass6 10334  mdslj1i 10527  mdslj2i 10528  mdslmd1lem1 10533  mdslmd2i 10538  irredlem3 10601  ghomf1olem 10681  toplat 10884  fipfil 11076  ordtypelem4 11430  ordtypelem7 11433  cnpnei 11472  subcls 11481  topfneec 11562  filrn 11643  limfilcf 11683  flimcls 11684  rnelfmlem 11698  fmfnfmlem1 11700  fmfnfmlem3 11702  fclusnei 11719  fcluscf 11724  fcluscomplem 11732  fclusfnei 11738  tailfb 11762  filnetlem3 11765  isga 11772  metf1o 11907  blhalf 11911  mettrifi 11912  geomcau 11914  iccss2 11921  iccshftr 11922  iccshftl 11924  iccdil 11926  icccntr 11928  icoopnst 11940  lincmb01cmp 11942  sub2cncf 11947  txbas 11973  uptx 11978  txcn 11979  sstotbnd 11992  rrnmet 12072  rrncms 12075  phtpycolem4 12096  phtpcer 12104

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 145  df-an 223  df-3an 783

Copyright terms: Public domain