Theorem 3expb 1199

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  3adant3r1  1207  3adant3r2  1208  3adant3r3  1209  3adant1l  1225  3adant1r  1226  mp3an1  1319  soinxp  4681  sotri  5006  fnfco  5372  mpoeq3dva  5917  fovrnda  5996  ovelrn  6001  fnmpoovd  6194  nnmsucr  6467  fidifsnid  6849  exmidpw  6886  undiffi  6902  fidcenumlemim  6929  ltpopr  7557  ltexprlemdisj  7568  recexprlemdisj  7592  mul4  8051  add4  8080  2addsub  8133  addsubeq4  8134  subadd4  8163  muladd  8303  ltleadd  8365  divmulap  8592  divap0  8601  div23ap  8608  div12ap  8611  divsubdirap  8625  divcanap5  8631  divmuleqap  8634  divcanap6  8636  divdiv32ap  8637  div2subap  8754  letrp1  8764  lemul12b  8777  lediv1  8785  cju  8877  nndivre  8914  nndivtr  8920  nn0addge1  9181  nn0addge2  9182  peano2uz2  9319  uzind  9323  uzind3  9325  fzind  9327  fnn0ind  9328  uzind4  9547  qre  9584  irrmul  9606  rpdivcl  9636  rerpdivcl  9641  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  fzaddel  10015  fzrev  10040  frec2uzf1od  10362  expdivap  10527  2shfti  10795  iooinsup  11240  isermulc2  11303  dvds2add  11787  dvds2sub  11788  dvdstr  11790  alzdvds  11814  divalg2  11885  lcmgcdlem  12031  lcmgcdeq  12037  isprm6  12101  pcqcl  12260  mgmplusf  12620  grprinvd  12640  ismndd  12673  idmhm  12692  submid  12699  0mhm  12704  mhmco  12705  mhmima  12706  grpinvcnv  12767  grpinvnzcl  12771  tgclb  12859  topbas  12861  neissex  12959  cnpnei  13013  txcnp  13065  psmetxrge0  13126  psmetlecl  13128  xmetlecl  13161  xmettpos  13164  elbl3ps  13188  elbl3  13189  metss  13288  comet  13293  bdxmet  13295  bdmet  13296  bl2ioo  13336  divcnap  13349  cncffvrn  13363  divccncfap  13371  dvrecap  13471  cosz12  13495