Theorem 3expb 1230

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  3adant3r1  1238  3adant3r2  1239  3adant3r3  1240  3adant1l  1256  3adant1r  1257  mp3an1  1360  soinxp  4796  sotri  5132  fnfco  5511  mpoeq3dva  6085  fovcdmda  6166  ovelrn  6171  fnmpoovd  6380  nnmsucr  6656  fidifsnid  7058  exmidpw  7100  undiffi  7117  fidcenumlemim  7151  ltpopr  7815  ltexprlemdisj  7826  recexprlemdisj  7850  mul4  8311  add4  8340  2addsub  8393  addsubeq4  8394  subadd4  8423  muladd  8563  ltleadd  8626  divmulap  8855  divap0  8864  div23ap  8871  div12ap  8874  divsubdirap  8888  divcanap5  8894  divmuleqap  8897  divcanap6  8899  divdiv32ap  8900  div2subap  9017  letrp1  9028  lemul12b  9041  lediv1  9049  cju  9141  nndivre  9179  nndivtr  9185  nn0addge1  9448  nn0addge2  9449  peano2uz2  9587  uzind  9591  uzind3  9593  fzind  9595  fnn0ind  9596  uzind4  9822  qre  9859  irrmul  9881  rpdivcl  9914  rerpdivcl  9919  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzaddel  10294  fzrev  10319  frec2uzf1od  10669  expdivap  10853  fundm2domnop0  11113  swrdwrdsymbg  11249  ccatpfx  11286  swrdccat  11320  2shfti  11409  iooinsup  11855  isermulc2  11918  dvds2add  12404  dvds2sub  12405  dvdstr  12407  alzdvds  12433  divalg2  12505  lcmgcdlem  12667  lcmgcdeq  12673  isprm6  12737  pcqcl  12897  mgmplusf  13467  grpinva  13487  ismndd  13538  imasmnd2  13553  idmhm  13570  issubm2  13574  submid  13578  0mhm  13587  resmhm  13588  resmhm2  13589  resmhm2b  13590  mhmco  13591  mhmima  13592  gsumwsubmcl  13597  gsumwmhm  13599  grpinvcnv  13669  grpinvnzcl  13673  grpsubf  13680  imasgrp2  13715  qusgrp2  13718  mhmfmhm  13722  mulgnnsubcl  13739  mulgnn0z  13754  mulgnndir  13756  issubg4m  13798  isnsg3  13812  nsgid  13820  qusadd  13839  ghmmhm  13858  ghmmhmb  13859  idghm  13864  resghm  13865  ghmf1  13878  kerf1ghm  13879  qusghm  13887  ghmfghm  13931  invghm  13934  ablnsg  13939  srgfcl  14005  srgmulgass  14021  srglmhm  14025  srgrmhm  14026  ringlghm  14093  ringrghm  14094  opprringbg  14112  mulgass3  14117  isnzr2  14217  subrngringnsg  14238  issubrng2  14243  issubrg2  14274  domnmuln0  14306  islmodd  14326  lmodscaf  14343  lcomf  14360  rmodislmodlem  14383  issubrgd  14485  qusrhm  14561  qusmul2  14562  crngridl  14563  qusmulrng  14565  znidom  14690  psraddcl  14713  tgclb  14808  topbas  14810  neissex  14908  cnpnei  14962  txcnp  15014  psmetxrge0  15075  psmetlecl  15077  xmetlecl  15110  xmettpos  15113  elbl3ps  15137  elbl3  15138  metss  15237  comet  15242  bdxmet  15244  bdmet  15245  bl2ioo  15293  divcnap  15308  cncfcdm  15325  divccncfap  15333  dvrecap  15456  dvmptfsum  15468  cosz12  15523  gausslemma2dlem1a  15806  usgredg2vlem1  16092  usgredg2vlem2  16093