Theorem 3expb 1228

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

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

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 1004

This theorem is referenced by:  3adant3r1  1236  3adant3r2  1237  3adant3r3  1238  3adant1l  1254  3adant1r  1255  mp3an1  1358  soinxp  4789  sotri  5124  fnfco  5500  mpoeq3dva  6068  fovcdmda  6149  ovelrn  6154  fnmpoovd  6361  nnmsucr  6634  fidifsnid  7033  exmidpw  7070  undiffi  7087  fidcenumlemim  7119  ltpopr  7782  ltexprlemdisj  7793  recexprlemdisj  7817  mul4  8278  add4  8307  2addsub  8360  addsubeq4  8361  subadd4  8390  muladd  8530  ltleadd  8593  divmulap  8822  divap0  8831  div23ap  8838  div12ap  8841  divsubdirap  8855  divcanap5  8861  divmuleqap  8864  divcanap6  8866  divdiv32ap  8867  div2subap  8984  letrp1  8995  lemul12b  9008  lediv1  9016  cju  9108  nndivre  9146  nndivtr  9152  nn0addge1  9415  nn0addge2  9416  peano2uz2  9554  uzind  9558  uzind3  9560  fzind  9562  fnn0ind  9563  uzind4  9783  qre  9820  irrmul  9842  rpdivcl  9875  rerpdivcl  9880  iccshftr  10190  iccshftl  10192  iccdil  10194  icccntr  10196  fzaddel  10255  fzrev  10280  frec2uzf1od  10628  expdivap  10812  fundm2domnop0  11067  swrdwrdsymbg  11196  ccatpfx  11233  swrdccat  11267  2shfti  11342  iooinsup  11788  isermulc2  11851  dvds2add  12336  dvds2sub  12337  dvdstr  12339  alzdvds  12365  divalg2  12437  lcmgcdlem  12599  lcmgcdeq  12605  isprm6  12669  pcqcl  12829  mgmplusf  13399  grpinva  13419  ismndd  13470  imasmnd2  13485  idmhm  13502  issubm2  13506  submid  13510  0mhm  13519  resmhm  13520  resmhm2  13521  resmhm2b  13522  mhmco  13523  mhmima  13524  gsumwsubmcl  13529  gsumwmhm  13531  grpinvcnv  13601  grpinvnzcl  13605  grpsubf  13612  imasgrp2  13647  qusgrp2  13650  mhmfmhm  13654  mulgnnsubcl  13671  mulgnn0z  13686  mulgnndir  13688  issubg4m  13730  isnsg3  13744  nsgid  13752  qusadd  13771  ghmmhm  13790  ghmmhmb  13791  idghm  13796  resghm  13797  ghmf1  13810  kerf1ghm  13811  qusghm  13819  ghmfghm  13863  invghm  13866  ablnsg  13871  srgfcl  13936  srgmulgass  13952  srglmhm  13956  srgrmhm  13957  ringlghm  14024  ringrghm  14025  opprringbg  14043  mulgass3  14048  isnzr2  14148  subrngringnsg  14169  issubrng2  14174  issubrg2  14205  domnmuln0  14237  islmodd  14257  lmodscaf  14274  lcomf  14291  rmodislmodlem  14314  issubrgd  14416  qusrhm  14492  qusmul2  14493  crngridl  14494  qusmulrng  14496  znidom  14621  psraddcl  14644  tgclb  14739  topbas  14741  neissex  14839  cnpnei  14893  txcnp  14945  psmetxrge0  15006  psmetlecl  15008  xmetlecl  15041  xmettpos  15044  elbl3ps  15068  elbl3  15069  metss  15168  comet  15173  bdxmet  15175  bdmet  15176  bl2ioo  15224  divcnap  15239  cncfcdm  15256  divccncfap  15264  dvrecap  15387  dvmptfsum  15399  cosz12  15454  gausslemma2dlem1a  15737  usgredg2vlem1  16020  usgredg2vlem2  16021