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

Theorem 3expia 1205
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expia  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1202 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 124 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
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 980
This theorem is referenced by:  mp3an3  1326  3gencl  2771  moi  2920  sotricim  4319  elirr  4536  en2lp  4549  suc11g  4552  3optocl  4700  sefvex  5531  f1oresrab  5676  ovmpos  5991  ov2gf  5992  poxp  6226  brtposg  6248  dfsmo2  6281  smoiun  6295  tfrlemibxssdm  6321  tfr1onlemsucfn  6334  tfr1onlemsucaccv  6335  tfr1onlembxssdm  6337  tfr1onlembfn  6338  tfr1onlemaccex  6342  tfr1onlemres  6343  tfrcllemsucfn  6347  tfrcllemsucaccv  6348  tfrcllembxssdm  6350  tfrcllembfn  6351  tfrcllemaccex  6355  tfrcllemres  6356  tfrcl  6358  nnsucsssuc  6486  nnaordi  6502  nnawordex  6523  mapvalg  6651  pmvalg  6652  elmapg  6654  xpdom3m  6827  ordiso  7028  ctssdc  7105  pr2ne  7184  ltbtwnnqq  7392  prarloclem4  7475  addlocpr  7513  1idprl  7567  1idpru  7568  ltexprlemrnd  7582  recexprlemrnd  7606  recexprlem1ssl  7610  recexprlem1ssu  7611  recexprlemss1l  7612  recexprlemss1u  7613  aptisr  7756  axpre-apti  7862  ltxrlt  8000  axapti  8005  lttri3  8014  reapti  8513  apreap  8521  msqge0  8550  mulge0  8553  recexap  8586  mulap0b  8588  lt2msq  8819  zaddcl  9269  zdiv  9317  zextlt  9321  prime  9328  uzind2  9341  fzind  9344  lbzbi  9592  xltneg  9810  xlt2add  9854  iocssre  9927  icossre  9928  iccssre  9929  fzen  10016  rebtwn2zlemshrink  10227  qbtwnxr  10231  ioo0  10233  ioom  10234  ico0  10235  ioc0  10236  expclzaplem  10517  expnegzap  10527  expaddzap  10537  expmulzap  10539  omgadd  10753  shftuz  10797  cau3lem  11094  climuni  11272  efltim  11677  divalgb  11900  ndvdssub  11905  dvdsgcd  11983  lcmgcdlem  12047  qredeu  12067  isprm3  12088  prmdvdsexpr  12120  prmexpb  12121  fermltl  12204  coprimeprodsq  12227  pythagtrip  12253  pcpremul  12263  pcdvdsb  12289  pc2dvds  12299  ctinf  12401  mulgaddcom  12882  dvdsunit  13093  unitmulclb  13095  cnntr  13358  cncnp2m  13364  cnptoprest  13372  lmtopcnp  13383  cnmptcom  13431  hmeof1o  13442  blpnf  13533  blssps  13560  blss  13561  blssec  13571  neibl  13624  climcncf  13704  cnplimcim  13769  bj-peano4  14329  triap  14400
  Copyright terms: Public domain W3C validator