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  4791  sotri  5127  fnfco  5505  mpoeq3dva  6077  fovcdmda  6158  ovelrn  6163  fnmpoovd  6372  nnmsucr  6647  fidifsnid  7046  exmidpw  7086  undiffi  7103  fidcenumlemim  7135  ltpopr  7798  ltexprlemdisj  7809  recexprlemdisj  7833  mul4  8294  add4  8323  2addsub  8376  addsubeq4  8377  subadd4  8406  muladd  8546  ltleadd  8609  divmulap  8838  divap0  8847  div23ap  8854  div12ap  8857  divsubdirap  8871  divcanap5  8877  divmuleqap  8880  divcanap6  8882  divdiv32ap  8883  div2subap  9000  letrp1  9011  lemul12b  9024  lediv1  9032  cju  9124  nndivre  9162  nndivtr  9168  nn0addge1  9431  nn0addge2  9432  peano2uz2  9570  uzind  9574  uzind3  9576  fzind  9578  fnn0ind  9579  uzind4  9800  qre  9837  irrmul  9859  rpdivcl  9892  rerpdivcl  9897  iccshftr  10207  iccshftl  10209  iccdil  10211  icccntr  10213  fzaddel  10272  fzrev  10297  frec2uzf1od  10645  expdivap  10829  fundm2domnop0  11085  swrdwrdsymbg  11217  ccatpfx  11254  swrdccat  11288  2shfti  11363  iooinsup  11809  isermulc2  11872  dvds2add  12357  dvds2sub  12358  dvdstr  12360  alzdvds  12386  divalg2  12458  lcmgcdlem  12620  lcmgcdeq  12626  isprm6  12690  pcqcl  12850  mgmplusf  13420  grpinva  13440  ismndd  13491  imasmnd2  13506  idmhm  13523  issubm2  13527  submid  13531  0mhm  13540  resmhm  13541  resmhm2  13542  resmhm2b  13543  mhmco  13544  mhmima  13545  gsumwsubmcl  13550  gsumwmhm  13552  grpinvcnv  13622  grpinvnzcl  13626  grpsubf  13633  imasgrp2  13668  qusgrp2  13671  mhmfmhm  13675  mulgnnsubcl  13692  mulgnn0z  13707  mulgnndir  13709  issubg4m  13751  isnsg3  13765  nsgid  13773  qusadd  13792  ghmmhm  13811  ghmmhmb  13812  idghm  13817  resghm  13818  ghmf1  13831  kerf1ghm  13832  qusghm  13840  ghmfghm  13884  invghm  13887  ablnsg  13892  srgfcl  13957  srgmulgass  13973  srglmhm  13977  srgrmhm  13978  ringlghm  14045  ringrghm  14046  opprringbg  14064  mulgass3  14069  isnzr2  14169  subrngringnsg  14190  issubrng2  14195  issubrg2  14226  domnmuln0  14258  islmodd  14278  lmodscaf  14295  lcomf  14312  rmodislmodlem  14335  issubrgd  14437  qusrhm  14513  qusmul2  14514  crngridl  14515  qusmulrng  14517  znidom  14642  psraddcl  14665  tgclb  14760  topbas  14762  neissex  14860  cnpnei  14914  txcnp  14966  psmetxrge0  15027  psmetlecl  15029  xmetlecl  15062  xmettpos  15065  elbl3ps  15089  elbl3  15090  metss  15189  comet  15194  bdxmet  15196  bdmet  15197  bl2ioo  15245  divcnap  15260  cncfcdm  15277  divccncfap  15285  dvrecap  15408  dvmptfsum  15420  cosz12  15475  gausslemma2dlem1a  15758  usgredg2vlem1  16041  usgredg2vlem2  16042