ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3expb Unicode version

Theorem 3expb 1167
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
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1165 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 255 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 947
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 949
This theorem is referenced by:  3adant3r1  1175  3adant3r2  1176  3adant3r3  1177  3adant1l  1193  3adant1r  1194  mp3an1  1287  soinxp  4579  sotri  4904  fnfco  5267  mpoeq3dva  5803  fovrnda  5882  ovelrn  5887  grprinvd  5934  fnmpoovd  6080  nnmsucr  6352  fidifsnid  6733  exmidpw  6770  undiffi  6781  fidcenumlemim  6808  ltpopr  7371  ltexprlemdisj  7382  recexprlemdisj  7406  mul4  7862  add4  7891  2addsub  7944  addsubeq4  7945  subadd4  7974  muladd  8114  ltleadd  8176  divmulap  8403  divap0  8412  div23ap  8419  div12ap  8422  divsubdirap  8436  divcanap5  8442  divmuleqap  8445  divcanap6  8447  divdiv32ap  8448  div2subap  8564  letrp1  8574  lemul12b  8587  lediv1  8595  cju  8687  nndivre  8724  nndivtr  8730  nn0addge1  8991  nn0addge2  8992  peano2uz2  9126  uzind  9130  uzind3  9132  fzind  9134  fnn0ind  9135  uzind4  9351  qre  9385  irrmul  9407  rpdivcl  9435  rerpdivcl  9440  iccshftr  9745  iccshftl  9747  iccdil  9749  icccntr  9751  fzaddel  9807  fzrev  9832  frec2uzf1od  10147  expdivap  10312  2shfti  10571  iooinsup  11014  isermulc2  11077  dvds2add  11454  dvds2sub  11455  dvdstr  11457  alzdvds  11479  divalg2  11550  lcmgcdlem  11685  lcmgcdeq  11691  isprm6  11752  tgclb  12161  topbas  12163  neissex  12261  cnpnei  12315  txcnp  12367  psmetxrge0  12428  psmetlecl  12430  xmetlecl  12463  xmettpos  12466  elbl3ps  12490  elbl3  12491  metss  12590  comet  12595  bdxmet  12597  bdmet  12598  bl2ioo  12638  divcnap  12651  cncffvrn  12665  divccncfap  12673  dvrecap  12773  cosz12  12788
  Copyright terms: Public domain W3C validator