Theorem imp 350

Description: Importation inference. (The proof was 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

Step	Hyp	Ref	Expression
1		imp.1	. 2 |- (ph -> (ps -> ch))
2		impexp 347	. 2 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))
3	1, 2	mpbir 190	1 |- ((ph /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  impcom 351  pm3.33 357  pm3.34 358  pm3.35 359  pm5.31 360  imp31 362  imp32 363  imp4b 365  imp41 368  imp42 369  imp43 370  imp44 371  imp45 372  impac 387  adantl 388  adantr 389  adantll 392  adantlr 393  adantrl 394  adantrr 395  biimpa 416  biimpar 417  biimpac 418  biimparc 419  jaob 422  jaoian 425  jaodan 426  pm4.43 431  imdistani 443  sylan 448  sylan2 451  syldan 467  sylan9r 469  anabsi7 496  3imtr3g 550  ordi 594  jcad 598  orcanai 688  mpanl1 704  mpanl2 705  mpanr1 707  mpanr2 708  mpanlr1 709  pm4.82 737  3adantl1 801  3adantl2 802  3adantl3 803  3jcad 818  3expia 833  3an1rs 843  3imp1 844  3imp2 846  syl3anl1 870  syl3anl2 871  syl3anl3 872  3anidm12 879  3anidm23 881  3jaoian 886  3jaodan 887  mp3anl1 907  mp3anl2 908  mp3anl3 909  19.21ad 1055  19.26 1063  equtr2 1129  equs4 1146  dvelimfALT 1149  a4imt 1154  a4imed 1157  equvini 1164  equs5a 1193  ax11v2 1210  ax11b 1215  dfsb2 1220  hbsb4 1243  dvelimdf 1246  sbcom 1253  equvin 1270  ax11eq 1356  ax11el 1357  ax11indi 1360  ax11indalem 1361  ax11inda2ALT 1362  ax11inda 1364  a12stdy2 1366  a12lem1 1369  mopick 1426  moexex 1431  nelneq 1553  nelneq2 1554  r19.21advv 1713  r19.21bi 1717  r19.23ai 1734  r19.23advv 1741  r19.15 1745  rcla4va 1866  reu3 1921  ra4sbca 1988  ra4esbca 1989  csbexg 1998  ra4csbela 2032  ssel2 2054  sstr 2062  sspsstr 2141  psssstr 2142  neldif 2155  reuss2 2265  reupick 2269  ssne0 2295  ssdisj 2308  disjpss 2309  disjssun 2316  pssdifn0 2319  dedth2h 2377  dedth4h 2379  sspr 2466  prel12 2475  iineq2 2569  ssiun 2582  dtruALT 2738  pwssun 2816  poirr 2836  potr 2837  reuuni2f 2873  mouniss 2880  elpwunsn 2902  frirr 2914  wefrc 2933  wereu 2935  ordelss 2954  trssord 2955  nordeq 2957  ordelord 2960  tz7.7 2963  ordsseleq 2966  onfr 2976  ordtr2 2992  oninton 3002  oneqmini 3007  limelon 3022  trsuc 3045  ordsssuc2 3049  unizlim 3103  limuni3 3113  tfi 3116  limomss 3127  ordom 3131  peano5 3143  findsg 3147  tfinds 3151  tfindsg 3152  tfindsg2 3153  brrelex 3197  optocl 3225  elrel 3243  relop 3265  breldmg 3305  elreldm 3327  relimasn 3409  asymref2 3424  asymref2OLD 3426  funopg 3533  funssres 3538  fununi 3549  funimass2 3559  fneu 3578  fnun 3580  fss 3620  fco 3621  opelf 3625  f1oun 3691  f1dmex 3695  fv3 3718  funopfvg 3737  fvelima 3749  fvelimab 3750  fvco 3759  fvco2 3760  fvopab3ig 3763  elrnopabg 3785  dff2 3802  funfvima2 3838  funfvima3 3839  isorel 3879  isocnv 3881  isotr 3882  isotrALT 3883  isomin 3884  isoini 3885  isofrlem 3886  f1oweALT 3891  tfrlem2 3897  tfrlem7 3902  tfrlem8 3903  tfrlem9 3904  tfrlem11 3906  tfr3 3911  rdglimt 3933  tz7.49 3944  abianfp 3947  ndmoprgOLD 4029  ndmoprcl 4030  1stdm 4093  oevn0 4138  oaordi 4164  oawordeu 4173  oawordexr 4174  oalimcl 4178  oaass 4179  oarec 4180  omordi 4181  omcan 4184  omwordri 4187  omword1 4188  omlimcl 4193  odi 4194  omass 4195  oeordi 4198  oecan 4200  oewordi 4202  oewordri 4203  oeordsuc 4205  nnacom 4217  nnmcom 4225  oaabs 4236  omsmolem 4240  omsmo 4241  ecoptocl 4287  eceqopreq 4297  th3qlem1 4298  th3qlem2 4299  f1oen2g 4375  en3d 4382  dom2d 4385  fundmen 4409  undom 4418  xpdom2 4422  pw2en 4426  sbthlem1 4427  ensdomtr 4451  domsdomtr 4456  enen1 4457  enen2 4458  domen1 4459  domen2 4460  sdomen1 4461  sdomen2 4462  fodomr 4463  mapenlem2 4470  mapen 4471  mapdom2 4474  mapunen 4482  nneneq 4492  php 4493  php3 4495  finsucdom 4506  pssinf 4507  isfinite1 4510  infsdomnn 4511  pssnn 4513  ssfi 4515  domfi 4516  unblem3 4519  isfinite2 4523  unfilem1 4524  unifi 4532  fiint 4534  abfii4 4538  fodomfi 4540  fodomfib 4541  pm54.43 4546  supmo 4550  supnub 4556  suppr 4562  suc11reg 4577  inf3lem1 4585  inf3lem5 4589  inf3lem6 4590  unbnnt 4611  zfregs 4619  setind 4620  r1ord 4627  r1val1 4630  tz9.12lem3 4633  rankr1 4646  ssrankr1 4648  rankxplim3 4686  rankxpsuc 4687  aceq3 4705  aceq5lem4 4710  aceq5 4712  aceq6b 4714  ac6s 4728  numthlem 4755  zorn2lem1 4760  zorn2lem4 4763  zorn2lem5 4764  zorn2lem6 4765  zorn2lem7 4766  fodomb 4772  unidom 4780  uniimadom 4782  sucdom 4814  unxpdomlem 4815  cardlim 4823  ondomon 4828  carduni 4830  alephordi 4846  alephle 4856  cardaleph 4857  cardinfima 4863  alephval2 4874  alephval3 4875  cflim 4881  axrepndlem1 4916  axrepndlem2 4917  axrepnd 4918  axpowndlem4 4924  axinfndlem1 4929  axacndlem4 4934  axacndlem5 4935  axacnd 4936  mulclpi 4993  mulcanpi 4999  ltmpi 5003  indpi 5006  ltaddpq 5051  ltrpq 5057  elprpq 5067  prcdpq 5069  distrlem4pr 5102  psslinpr 5107  prlem934a 5109  prlem934 5111  ltaddpr 5112  ltexprlem3 5116  ltexprlem5 5118  ltaprlem 5122  prlem936 5127  suplem1pr 5133  mulcmpblnr 5155  recexsrlem 5184  mulgt0sr 5186  ssgt0sr 5189  suppsrlem 5193  suppsr2 5195  suppsr3 5196  suprelem 5231  axrrecex 5256  cnegextlem1 5317  cnegextlem2 5318  addcan 5323  renegcl 5388  letrt 5498  xrletrt 5537  xrret 5542  xrre2t 5543  addgegt0 5574  msqgt0t 5589  gt0ne0t 5592  addgt0t 5620  addgegt0t 5621  addge0t 5623  mulge0t 5652  recext 5657  mulcan 5659  mulcan2t 5662  divmult 5676  recne0t 5695  recidt 5698  div23t 5705  div13t 5706  div12t 5707  divdirt 5713  divmuldivt 5736  divadddivt 5740  divdivdivt 5741  redivcl 5754  prodgt0 5775  prodge0 5776  prodgt0t 5782  prodgt02t 5783  prodge0t 5784  prodge02t 5785  ltmul1t 5786  ltmul12it 5797  lemul12itOLD 5799  mulgt1t 5801  ltdiv1t 5805  lediv1t 5806  ltmuldivt 5817  ltmuldiv2t 5818  ltdivmult 5819  ledivmult 5820  lemuldiv2t 5825  ltrect 5832  lerect 5833  lt2msqt 5834  lediv12it 5844  le2msqt 5851  ledivp1t 5853  ledivp1 5854  ltdivp1 5855  lt1nnn 5895  nnleltp1t 5901  nndivtrt 5907  lble 5994  sup2 5998  suprub 6003  suprlub 6004  suprnub 6005  suprleub 6006  infmrcl 6016  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxr 6028  supxrre 6030  supxrun 6032  supxrunb1 6036  supxrunb2 6037  supxrbnd 6038  supxrub 6045  supxrleub 6046  dfn2 6059  lt0nnn0 6063  nnnn0addclt 6072  elnnz 6092  elnnz1 6102  nn0subt 6108  zaddclt 6112  zmulclt 6127  zltp1let 6128  btwnnzt 6139  zneo 6147  zneoOLD 6148  uzind2 6154  uzindOLD 6156  uzwo4OLD 6158  nn0ind-raph 6162  zbtwnre 6169  qaddclt 6207  qmulclt 6209  qrecclt 6211  qbtwnre 6216  qsqueeze 6218  rpmulclt 6228  monoord 6231  seq1rn2 6258  ser1add2 6275  ser1add 6276  iooss1 6310  iooss2 6311  elioo4g 6318  iccsupr 6331  icoshft 6341  icounlem 6345  icoun 6346  eluzt 6358  uz11t 6364  eluzp1m1t 6365  uzwo 6387  uzwoOLD 6388  elfzel2g 6412  elfz2nn0t 6427  elfz3nn0t 6429  fznn0subt 6430  fsequb 6455  fsequb2 6456  fseqsupcl 6457  fseqsupub 6458  seqzfveq 6486  seqzrn2 6488  expp1t 6506  expordit 6531  expcant 6532  expordt 6533  expword2it 6536  exple1t 6538  expubndt 6539  sq11t 6560  sq01t 6582  expnbndt 6585  sqr0 6602  sqrlem12 6614  sqrclt 6640  sqrgt0t 6641  sqrge0t 6642  sqrlet 6643  sqr00t 6644  sqrsqt 6652  sqsqrt 6653  crulem 6666  replimt 6692  absrpclt 6790  absidt 6797  absnidt 6798  leabst 6799  abssubne0t 6820  seq1bnd 6847  cau2 6850  cau5i 6854  cvg3 6860  caubnd 6863  faclbnd 6882  faclbnd4lem4 6888  bccl2t 6909  climcl 6916  sumeq2 6923  fsum1s 6947  fsum1s2 6948  fsump1s 6951  fsumcllem 6952  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  fsumcom 6966  fsumrev 6967  fsumshftm 6970  fsummulc1 6971  fsummulc2 6972  fsumdivc 6973  fsumdivcALT 6974  fsumconst 6976  fsumcmp 6978  fsumcmpndx2 6980  fsumabs 6981  clm3 7017  clm4le 7019  clm0 7021  clm0nns 7023  clmi2at 7029  climconst 7031  climunii 7035  2climnn 7039  2climnn0 7040  climshft 7041  iserzshft2 7044  climge0 7049  climaddc1 7054  climaddc2 7055  climmullem4 7059  climmullem5 7060  climmulc2 7065  climsubc2 7067  clim2serzt 7070  climcmplem 7073  climserzle 7083  climcau 7092  caucvglem2 7094  caucvglem6 7098  caucvg 7099  serzf0 7105  ser1f0 7106  ser1cmp2 7113  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  cvgcmp3cet 7126  isumclim2tf 7133  isumclt 7144  iserzgt0 7146  isumcmpi 7150  reccnv 7153  infcvglem3 7158  expcnv 7168  georeclim 7175  geoisumr 7178  cvgratlem2ALT 7183  cvgratlem3ALT 7184  cvgratlem1 7185  cvgratlem2 7186  cvgratlem3 7187  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag3 7195  fsum0diag4 7196  elcncf 7200  elcncf1d 7205  ivthlem9 7224  efaddlem23 7302  eftlext 7320  reeff1o 7368  xpnnen 7441  znnen 7445  unbenlem 7447  infpnlem1 7449  infxpidmlem7 7501  infxpidmlem10 7504  infxpidmlem11 7505  infmap2lem1 7521  alephexp1 7526  uniopnt 7540  tgclt 7566  tgss2t 7579  basgen2t 7581  subbas2 7587  subtop 7588  fctop 7592  cctop 7594  retopbas 7597  ntrval 7618  iincld 7621  clsval2 7627  0ntr 7644  elcls 7646  elcls3 7652  neii1 7662  neii2 7663  0nnei 7667  islp2 7688  clslp 7689  qdensere 7691  cnima 7706  cnclima 7710  cnsscnp 7711  cncnplem4 7716  cncnp 7717  metxplem3 7768  metxplem4 7773  metxp 7774  rnblssm 7791  blss 7793  ssbl 7795  opnuni 7808  opnin 7809  rnblopn 7814  metcnp 7826  metcn 7828  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metcnss2 7838  metdnsconst 7840  cncfmet 7844  lmnn 7873  caun0 7880  lmsslem 7887  caussi 7889  metelcls 7900  metcnp4 7904  metcn4i 7906  xplmi 7907  xplm 7909  xpcn 7910  iscms2lem3 7925  iscms2lem4 7926  iscms2lem5 7927  lmcau 7930  cmsss 7931  bcthlem2 7934  bcthlem10 7942  bcthlem21 7953  bcthlem25 7957  bcthlem28 7960  bcthlem33 7965  bcth 7966  grpass 7981  grpidinvlem3 7984  grpidinvlem4 7985  grpid 7999  grpasscan1OLD 8008  grpasscan1 8012  grpnnncan2 8028  grplactf1o 8034  subgabl 8060  ghgrpilem2 8071  nvz 8236  nvcni 8266  nvlmle 8268  sspmval 8326  sspival 8331  sspimsval 8333  nmoub3i 8368  nmobndseqi 8372  nmlno0lem 8385  nmlnoubi 8388  nmblolbi 8391  isblo3i 8392  blocni 8396  ipasslem1 8421  ipasslem5 8425  ipdir 8433  ipass 8436  ipsubdir 8439  sspph 8446  ubthlem5 8464  ubthlem14 8473  ubthi 8475  htthlem7 8556  htthlem10 8559  htthlem12 8561  psref 8575  spwmo 8580  efifolem2 8638  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  normpyct 8934  shelt 9001  shsubcltOLD 9011  chelt 9021  hlimcaui 9027  ocorth 9080  shorth 9084  ocnelt 9086  occl 9097  projlem13 9114  projlem15 9116  projlem26 9127  projlem27 9128  projlem28 9129  pjthlem13 9146  pjtheut 9151  pjpj0 9170  pjomlt 9184  shscl 9196  shsel1t 9200  chintcl 9210  shlej1t 9270  shmods 9277  shmod 9278  h1dn0 9390  spansn 9396  spansnmul 9403  spansnsst 9411  elspansn4t 9413  h1datom 9421  cm2jt 9480  osumlem4 9498  osumlem6 9500  spansncv 9514  5oalem6 9521  pjige0t 9553  pjsumt 9572  pjds 9574  pjds3 9575  homco1t 9644  homulasst 9645  eigret 9678  eigortht 9681  nmopub2tALT 9750  nmfnleub2t 9766  elnlfn2t 9769  kbpjt 9796  homco2t 9817  nmlnop0ALT 9835  nmopunt 9854  nmbdoplbt 9865  nmcopexlem1 9866  nmcopexlem6 9871  nmcoplbt 9875  nmcfnexlem1 9895  nmcfnexlem6 9900  nmcfnlbt 9904  nlelch 9909  branmfnt 9951  bra11 9954  cnvbravalt 9956  leopaddt 9977  leopmulit 9978  leopmul2it 9980  pjnmop 9986  pjnormss 10007  pjclem4 10037  pj3s 10045  hstel2t 10056  hst1ht 10064  stle 10077  stles 10078  stadd 10083  stadd3 10085  strlem3a 10089  hstrlem3a 10097  stcltrlem1 10113  spansncv2t 10130  mdslmd1lem3 10162  mdslmd1lem4 10163  csmdsym 10169  mdexch 10170  atss 10181  atsseq 10182  superpos 10189  chcv1t 10190  chjatom 10192  hatomict 10195  hatomistic 10197  cvbr3 10202  atcv1t 10215  atexcht 10216  atoml 10217  atoml2 10218  atcvatlem 10220  atcvat 10221  atcvat2 10222  irredlem3 10227  irredlem4 10228  atcvat3 10231  atcvat4 10232  mdsymlem3 10240  sumdmdi 10249  sumdmdlem 10252  sumdmdlem2 10253  dmdbr5at 10255  cdj1 10265  cdj3lem1 10266  cdj3lem2b 10269  ghomgsg 10300  ghomf1olem 10301  findabrcl 10325  uninqs 10342  infi1 10347  ficli 10368  f2imacnv 10370  oooeqim2 10371  cdrci 10381  truni1 10386  esnnei 10395  hmeomap 10405  hmeocna 10406  hmeocnb 10407  cmphmp 10408  cnvhmpha 10412  cnvhmphb 10413  hmphre 10417  hmphtr 10418  hmeogrp 10425  homcard 10426  qusp 10430  filint 10437  fipfil2 10439  fgsb 10444  efilcp 10445  infi 10448  fgsb2 10449  efilcp2 10450  cnfilca 10451  iintlem1 10476  trnij 10481  idosd 10521  rdmob 10525  cmpasso 10550  cmpassoh 10573  homgrf 10574  imonclem 10583  ismonc 10584  cmpmon 10585  icmpmon 10587  idmon 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain