Theorem 3expb 1183

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

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

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 965

This theorem is referenced by:  3adant3r1  1191  3adant3r2  1192  3adant3r3  1193  3adant1l  1209  3adant1r  1210  mp3an1  1303  soinxp  4617  sotri  4942  fnfco  5305  mpoeq3dva  5843  fovrnda  5922  ovelrn  5927  grprinvd  5974  fnmpoovd  6120  nnmsucr  6392  fidifsnid  6773  exmidpw  6810  undiffi  6821  fidcenumlemim  6848  ltpopr  7427  ltexprlemdisj  7438  recexprlemdisj  7462  mul4  7918  add4  7947  2addsub  8000  addsubeq4  8001  subadd4  8030  muladd  8170  ltleadd  8232  divmulap  8459  divap0  8468  div23ap  8475  div12ap  8478  divsubdirap  8492  divcanap5  8498  divmuleqap  8501  divcanap6  8503  divdiv32ap  8504  div2subap  8620  letrp1  8630  lemul12b  8643  lediv1  8651  cju  8743  nndivre  8780  nndivtr  8786  nn0addge1  9047  nn0addge2  9048  peano2uz2  9182  uzind  9186  uzind3  9188  fzind  9190  fnn0ind  9191  uzind4  9410  qre  9444  irrmul  9466  rpdivcl  9496  rerpdivcl  9501  iccshftr  9807  iccshftl  9809  iccdil  9811  icccntr  9813  fzaddel  9870  fzrev  9895  frec2uzf1od  10210  expdivap  10375  2shfti  10635  iooinsup  11078  isermulc2  11141  dvds2add  11563  dvds2sub  11564  dvdstr  11566  alzdvds  11588  divalg2  11659  lcmgcdlem  11794  lcmgcdeq  11800  isprm6  11861  tgclb  12273  topbas  12275  neissex  12373  cnpnei  12427  txcnp  12479  psmetxrge0  12540  psmetlecl  12542  xmetlecl  12575  xmettpos  12578  elbl3ps  12602  elbl3  12603  metss  12702  comet  12707  bdxmet  12709  bdmet  12710  bl2ioo  12750  divcnap  12763  cncffvrn  12777  divccncfap  12785  dvrecap  12885  cosz12  12909