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

Theorem 3expia 1184
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 1181 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 123 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
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:  mp3an3  1305  3gencl  2723  moi  2870  sotricim  4252  elirr  4463  en2lp  4476  suc11g  4479  3optocl  4624  sefvex  5449  f1oresrab  5592  ovmpos  5901  ov2gf  5902  poxp  6136  brtposg  6158  dfsmo2  6191  smoiun  6205  tfrlemibxssdm  6231  tfr1onlemsucfn  6244  tfr1onlemsucaccv  6245  tfr1onlembxssdm  6247  tfr1onlembfn  6248  tfr1onlemaccex  6252  tfr1onlemres  6253  tfrcllemsucfn  6257  tfrcllemsucaccv  6258  tfrcllembxssdm  6260  tfrcllembfn  6261  tfrcllemaccex  6265  tfrcllemres  6266  tfrcl  6268  nnsucsssuc  6395  nnaordi  6411  nnawordex  6431  mapvalg  6559  pmvalg  6560  elmapg  6562  xpdom3m  6735  ordiso  6928  ctssdc  7005  pr2ne  7064  ltbtwnnqq  7246  prarloclem4  7329  addlocpr  7367  1idprl  7421  1idpru  7422  ltexprlemrnd  7436  recexprlemrnd  7460  recexprlem1ssl  7464  recexprlem1ssu  7465  recexprlemss1l  7466  recexprlemss1u  7467  aptisr  7610  axpre-apti  7716  ltxrlt  7853  axapti  7858  lttri3  7867  reapti  8364  apreap  8372  msqge0  8401  mulge0  8404  recexap  8437  mulap0b  8439  lt2msq  8667  zaddcl  9117  zdiv  9162  zextlt  9166  prime  9173  uzind2  9186  fzind  9189  lbzbi  9434  xltneg  9648  xlt2add  9692  iocssre  9765  icossre  9766  iccssre  9767  fzen  9853  rebtwn2zlemshrink  10061  qbtwnxr  10065  ioo0  10067  ioom  10068  ico0  10069  ioc0  10070  expclzaplem  10347  expnegzap  10357  expaddzap  10367  expmulzap  10369  omgadd  10579  shftuz  10620  cau3lem  10917  climuni  11093  efltim  11439  divalgb  11656  ndvdssub  11661  dvdsgcd  11734  lcmgcdlem  11792  qredeu  11812  isprm3  11833  prmdvdsexpr  11862  prmexpb  11863  ctinf  11977  cnntr  12431  cncnp2m  12437  cnptoprest  12445  lmtopcnp  12456  cnmptcom  12504  hmeof1o  12515  blpnf  12606  blssps  12633  blss  12634  blssec  12644  neibl  12697  climcncf  12777  cnplimcim  12842  bj-peano4  13322  triap  13397
  Copyright terms: Public domain W3C validator