Theorem 3expb 1206

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

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

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 982

This theorem is referenced by:  3adant3r1  1214  3adant3r2  1215  3adant3r3  1216  3adant1l  1232  3adant1r  1233  mp3an1  1335  soinxp  4729  sotri  5061  fnfco  5428  mpoeq3dva  5982  fovcdmda  6062  ovelrn  6067  fnmpoovd  6268  nnmsucr  6541  fidifsnid  6927  exmidpw  6964  undiffi  6981  fidcenumlemim  7011  ltpopr  7655  ltexprlemdisj  7666  recexprlemdisj  7690  mul4  8151  add4  8180  2addsub  8233  addsubeq4  8234  subadd4  8263  muladd  8403  ltleadd  8465  divmulap  8694  divap0  8703  div23ap  8710  div12ap  8713  divsubdirap  8727  divcanap5  8733  divmuleqap  8736  divcanap6  8738  divdiv32ap  8739  div2subap  8856  letrp1  8867  lemul12b  8880  lediv1  8888  cju  8980  nndivre  9018  nndivtr  9024  nn0addge1  9286  nn0addge2  9287  peano2uz2  9424  uzind  9428  uzind3  9430  fzind  9432  fnn0ind  9433  uzind4  9653  qre  9690  irrmul  9712  rpdivcl  9745  rerpdivcl  9750  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  fzaddel  10125  fzrev  10150  frec2uzf1od  10477  expdivap  10661  2shfti  10975  iooinsup  11420  isermulc2  11483  dvds2add  11968  dvds2sub  11969  dvdstr  11971  alzdvds  11996  divalg2  12067  lcmgcdlem  12215  lcmgcdeq  12221  isprm6  12285  pcqcl  12444  mgmplusf  12949  grpinva  12969  ismndd  13018  idmhm  13041  issubm2  13045  submid  13049  0mhm  13058  resmhm  13059  resmhm2  13060  resmhm2b  13061  mhmco  13062  mhmima  13063  gsumwsubmcl  13068  gsumwmhm  13070  grpinvcnv  13140  grpinvnzcl  13144  grpsubf  13151  imasgrp2  13180  qusgrp2  13183  mhmfmhm  13187  mulgnnsubcl  13204  mulgnn0z  13219  mulgnndir  13221  issubg4m  13263  isnsg3  13277  nsgid  13285  qusadd  13304  ghmmhm  13323  ghmmhmb  13324  idghm  13329  resghm  13330  ghmf1  13343  kerf1ghm  13344  qusghm  13352  ghmfghm  13396  invghm  13399  ablnsg  13404  srgfcl  13469  srgmulgass  13485  srglmhm  13489  srgrmhm  13490  ringlghm  13557  ringrghm  13558  opprringbg  13576  mulgass3  13581  isnzr2  13680  subrngringnsg  13701  issubrng2  13706  issubrg2  13737  domnmuln0  13769  islmodd  13789  lmodscaf  13806  lcomf  13823  rmodislmodlem  13846  issubrgd  13948  qusrhm  14024  qusmul2  14025  crngridl  14026  qusmulrng  14028  znidom  14145  psraddcl  14164  tgclb  14233  topbas  14235  neissex  14333  cnpnei  14387  txcnp  14439  psmetxrge0  14500  psmetlecl  14502  xmetlecl  14535  xmettpos  14538  elbl3ps  14562  elbl3  14563  metss  14662  comet  14667  bdxmet  14669  bdmet  14670  bl2ioo  14710  divcnap  14723  cncfcdm  14737  divccncfap  14745  dvrecap  14862  cosz12  14915  gausslemma2dlem1a  15174