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

Theorem imp 119
Description: Importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
imp.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
imp  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem imp
StepHypRef Expression
1 simpl 106 . 2  |-  ( (
ph  /\  ps )  ->  ph )
2 simpr 107 . 2  |-  ( (
ph  /\  ps )  ->  ps )
3 imp.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3sylc 60 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem is referenced by:  impcom  120  impd  246  imp31  247  imp32  248  expdimp  250  impancom  251  pm3.22  256  ancoms  259  adantr  265  biimpa  284  biimpar  285  biimpac  286  biimparc  287  pm3.33  331  pm3.34  332  pm3.35  333  pm5.31  334  imp4b  336  imp41  339  imp42  340  imp43  341  imp44  342  imp45  343  imp5g  346  expr  361  impac  367  sylan9  395  sylan9r  396  imdistani  427  mpan10  451  anabsi5  521  anim12dan  542  pm3.43  544  con3dimp  574  imnan  634  jaoian  719  jaodan  721  impidc  766  pm2.5dc  774  con2bidc  780  pm5.18dc  788  dfandc  789  pm4.63dc  791  annimim  793  pm4.54dc  816  pm4.79dc  820  orcanai  848  annimdc  856  pm4.55dc  857  pm4.82  868  pm3.11dc  875  pm3.12dc  876  dn1dc  878  3jcad  1096  3expia  1117  3an1rs  1127  3imp1  1128  3imp2  1130  syl3anl2  1195  3jaoian  1211  3jaodan  1212  mp3anl1  1237  mp3anl2  1238  mp3anl3  1239  ecased  1255  xor3dc  1294  pm5.15dc  1296  xor2dc  1297  xornbidc  1298  xordc  1299  nbbndc  1301  biassdc  1302  bilukdc  1303  dfbi3dc  1304  pm5.24dc  1305  xordidc  1306  alanimi  1364  19.29  1527  equs4  1629  equsexd  1633  spimth  1639  equs5a  1691  ax11v2  1717  ax11b  1723  equs5or  1727  sb5rf  1748  equvin  1759  nfsb4t  1906  eu5  1963  mopick  1994  euexex  2001  2euswapdc  2007  exists2  2013  eqrdav  2055  dvelimdc  2213  nebidc  2300  pm13.18  2301  nelne1  2310  nelne2  2311  ralrimdvv  2420  r19.21bi  2424  r19.26  2458  ralbi  2462  rexbi  2463  r19.29  2467  vtoclgft  2621  rspcva  2671  rspc2va  2686  elabgt  2707  eqeu  2734  mob2  2744  mob  2746  euind  2751  reu6  2753  reuind  2767  sbctt  2852  rspsbca  2869  sbcnestgf  2925  rspcsbela  2933  ssel2  2968  sselda  2973  sstr  2981  nssne1  3029  nssne2  3030  reuss2  3245  reupick  3249  reupick2  3251  reximdva0m  3264  ssn0  3287  disjel  3302  ssdisj  3305  disjpss  3306  absneu  3470  preqr1g  3565  prel12  3570  dfiun2g  3717  nbrne1  3809  nbrne2  3810  mpteq12f  3865  triun  3895  csbexga  3913  iinexgm  3936  prexgOLD  3974  prexg  3975  copsex2t  4010  swopo  4071  poirr  4072  potr  4073  pofun  4077  issod  4084  ordelss  4144  trssord  4145  limelon  4164  trsuc  4187  eusvnfb  4214  rabxfrd  4229  regexmidlem1  4286  nordeq  4296  suc11g  4309  nnsuc  4366  brrelex12  4409  vtoclr  4416  optocl  4444  relop  4514  brcogw  4532  breldmg  4569  elreldm  4588  riinint  4621  issref  4735  xpidtr  4743  trin2  4744  cnveqb  4804  funopg  4962  funssres  4970  fununi  4995  funimass2  5005  imain  5009  fnun  5033  fco  5084  opelf  5090  f1oun  5174  fun11iun  5175  fv3  5225  ndmfvg  5232  fvelima  5253  fvopab3ig  5274  fvmptssdm  5283  fvmptf  5291  fvimacnv  5310  fmptco  5358  funfvima2  5419  funfvima3  5420  f1veqaeq  5436  f1ocnvfvrneq  5450  fliftfun  5464  isotr  5484  isoini  5485  isopolem  5489  isosolem  5491  moriotass  5524  acexmidlem2  5537  suppssfv  5736  suppssov1  5737  f1dmex  5771  releldm2  5839  f1o2ndf1  5877  poxp  5881  tposf2  5914  iunon  5930  smoel2  5949  tfrlem9  5966  tfrexlem  5979  tfri3  5984  sucinc2  6057  nnacom  6094  nnmcom  6099  nnsucsssuc  6102  nntri2or2  6107  nnaordi  6112  nnmordi  6120  nnaordex  6131  nnm00  6133  ectocld  6203  iinerm  6209  th3qlem2  6240  f1oen3g  6265  f1oeng  6268  en2d  6279  en3d  6280  dom2lem  6283  fundmen  6317  fundmeng  6318  unen  6324  xpdom2  6336  xpdom2g  6337  fopwdom  6341  nneneq  6351  phpm  6358  phpelm  6359  fin0  6373  findcard  6376  diffifi  6382  ac6sfi  6383  onunsnss  6386  isotilem  6410  ordiso2  6415  carden2bex  6427  ltmpig  6495  enq0sym  6588  addnq0mo  6603  mulnq0mo  6604  prarloclem3step  6652  prarloclem3  6653  genpml  6673  genpmu  6674  genprndl  6677  genprndu  6678  genpdisj  6679  distrlem1prl  6738  distrlem1pru  6739  distrlem4prl  6740  distrlem4pru  6741  distrlem5prl  6742  distrlem5pru  6743  ltsopr  6752  ltaddpr  6753  addcanprleml  6770  addcanprlemu  6771  recexprlemm  6780  recexprlemlol  6782  recexprlemupu  6784  aptiprleml  6795  aptiprlemu  6796  caucvgprlemnkj  6822  caucvgprlemnbj  6823  addsrmo  6886  mulsrmo  6887  srpospr  6925  caucvgsr  6944  axprecex  7012  mulgt0  7152  ltne  7162  cnegexlem1  7249  cnegexlem2  7250  addgt0  7517  addgegt0  7518  addgtge0  7519  addge0  7520  recexre  7643  mulge0  7684  recexap  7708  prodgt02  7894  prodge02  7896  ltmul12a  7901  mulgt1  7904  nndivtr  8031  addltmul  8218  elnnnn0b  8283  elnnz  8312  zmulcl  8355  nn0n0n1ge2  8369  nn0lt2  8380  uzind2  8409  nn0ind-raph  8414  eluzp1m1  8592  uz3m2nn  8611  negm  8647  lbzbi  8648  qaddcl  8667  qmulcl  8669  qreccl  8674  ledivge1le  8750  nn0ledivnn  8785  xrltne  8830  xrre  8834  xrre2  8835  xrre3  8836  ge0gtmnf  8837  xltnegi  8849  iccsupr  8936  icoshft  8959  icoshftf1o  8960  fznlem  9007  fzen  9009  uzsubsubfz  9013  fzsuc2  9043  elfz1b  9054  elfz0ubfz0  9084  elfz0fzfz0  9085  fz0fzelfz0  9086  fz0fzdiffz0  9089  elfzmlbmOLD  9091  elfzmlbp  9092  difelfznle  9095  fzofzim  9146  eluzgtdifelfzo  9155  elfzodifsumelfzo  9159  elfzonlteqm1  9168  elfzom1p1elfzo  9172  ssfzo12bi  9183  subfzo0  9199  modqmuladdnn0  9318  modfzo0difsn  9345  addmodlteq  9348  frec2uzlt2d  9354  frecuzrdgfn  9362  iseqid3  9409  m1expcl2  9442  expge1  9457  leexp2r  9474  expubnd  9477  zesq  9535  expnlbnd  9541  nn0opthd  9590  faclbnd  9609  bcpasc  9634  rexanuz  9815  rexuz3  9817  r19.29uz  9819  r19.2uz  9820  absnid  9900  leabs  9901  ltabs  9914  icodiamlt  10007  climcn2  10061  climcau  10097  climcaucn  10101  dvds0lem  10118  dvds2ln  10140  dvdssub2  10149  dvdsadd2b  10154  dvdsabseq  10159  divconjdvds  10161  dvdsdivcl  10162  odd2np1  10184  oddge22np1  10193  opoe  10207  omoe  10208  opeo  10209  omeo  10210  m1expo  10212  nn0ehalf  10215  nn0o1gt2  10217  nno  10218  divalgb  10237  ndvdsadd  10243  ialgfx  10274  bj-prexg  10418  peano5set  10451  peano5setOLD  10452  bj-peano4  10467  bj-nn0suc  10476  bj-nn0sucALT  10490  bj-findis  10491
  Copyright terms: Public domain W3C validator