Theorem 3expb 1194

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

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

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 970

This theorem is referenced by:  3adant3r1  1202  3adant3r2  1203  3adant3r3  1204  3adant1l  1220  3adant1r  1221  mp3an1  1314  soinxp  4673  sotri  4998  fnfco  5361  mpoeq3dva  5902  fovrnda  5981  ovelrn  5986  grprinvd  6033  fnmpoovd  6179  nnmsucr  6452  fidifsnid  6833  exmidpw  6870  undiffi  6886  fidcenumlemim  6913  ltpopr  7532  ltexprlemdisj  7543  recexprlemdisj  7567  mul4  8026  add4  8055  2addsub  8108  addsubeq4  8109  subadd4  8138  muladd  8278  ltleadd  8340  divmulap  8567  divap0  8576  div23ap  8583  div12ap  8586  divsubdirap  8600  divcanap5  8606  divmuleqap  8609  divcanap6  8611  divdiv32ap  8612  div2subap  8729  letrp1  8739  lemul12b  8752  lediv1  8760  cju  8852  nndivre  8889  nndivtr  8895  nn0addge1  9156  nn0addge2  9157  peano2uz2  9294  uzind  9298  uzind3  9300  fzind  9302  fnn0ind  9303  uzind4  9522  qre  9559  irrmul  9581  rpdivcl  9611  rerpdivcl  9616  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  fzaddel  9990  fzrev  10015  frec2uzf1od  10337  expdivap  10502  2shfti  10769  iooinsup  11214  isermulc2  11277  dvds2add  11761  dvds2sub  11762  dvdstr  11764  alzdvds  11788  divalg2  11859  lcmgcdlem  12005  lcmgcdeq  12011  isprm6  12075  pcqcl  12234  tgclb  12665  topbas  12667  neissex  12765  cnpnei  12819  txcnp  12871  psmetxrge0  12932  psmetlecl  12934  xmetlecl  12967  xmettpos  12970  elbl3ps  12994  elbl3  12995  metss  13094  comet  13099  bdxmet  13101  bdmet  13102  bl2ioo  13142  divcnap  13155  cncffvrn  13169  divccncfap  13177  dvrecap  13277  cosz12  13301