Theorem imp 348

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 345	. 2 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))
3	1, 2	mpbir 188	1 |- ((ph /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  impcom 349  pm3.33 355  pm3.34 356  pm3.35 357  pm5.31 358  imp31 360  imp32 361  imp4b 363  imp41 366  imp42 367  imp43 368  imp44 369  imp45 370  expdimp 375  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 432  imdistani 445  sylan 450  sylan2 453  syldan 469  sylan9r 471  anabsi7 500  3imtr3g 555  ordi 599  jcad 603  orcanai 694  mpanl1 710  mpanl2 711  mpanr1 713  mpanr2 714  mpanlr1 716  pm4.82 744  dn1 779  3adantl1 809  3adantl2 810  3adantl3 811  3jcad 826  3expia 841  3an1rs 851  3imp1 852  3imp2 854  syl3anl1 879  syl3anl2 880  syl3anl3 881  3anidm12 888  3anidm23 890  3jaoian 895  3jaodan 896  mp3anl1 916  mp3anl2 917  mp3anl3 918  19.21ad 1095  19.26 1103  equtr2 1170  equs4 1187  dvelimfALT 1190  a4imt 1195  a4imed 1198  equvini 1205  equs5a 1234  ax11v2 1252  ax11b 1257  dfsb2 1262  hbsb4 1286  dvelimdf 1289  sbcom 1296  equvin 1313  dvelimALT 1392  ax11eq 1402  ax11el 1403  ax11indi 1406  ax11indalem 1407  ax11inda2ALT 1408  ax11inda 1410  a12stdy2 1412  a12lem1 1415  mopick 1472  moexex 1478  eqrdav 1517  nelneq 1604  nelneq2 1605  r19.21advv 1767  r19.21bi 1771  r19.23ai 1788  r19.15 1799  rcla4va 1921  reu3 1977  ra4sbca 2048  ra4esbca 2049  csbexg 2059  ra4csbela 2094  ssel2 2116  sstr 2124  sspsstr 2203  psssstr 2204  neldif 2217  reuss2 2327  reupick 2331  ssn0 2358  ssdisj 2371  disjpss 2372  disjssun 2379  pssdifn0 2382  dedth2h 2441  dedth4h 2443  sspr 2540  prel12 2549  iineq2 2647  ssiun 2660  dtru 2831  pwssun 2905  poirr 2923  potr 2924  frirr 2954  wefrc 2970  wereu 2972  ordelss 2991  trssord 2992  nordeq 2994  ordelord 2997  tz7.7 3001  onfr 3014  ordtr2 3019  limelon 3036  trsuc 3056  ordsssuc2 3060  unizlim 3086  reuuni2f 3107  mouniss 3113  elpwunsn 3135  oninton 3157  limuni3 3206  tfi 3207  tfinds 3212  tfindsg 3213  tfindsg2 3214  limomss 3224  ordom 3228  peano5 3241  findsg 3245  brrelex 3290  optocl 3321  elrel 3342  relop 3365  opelxpex2 3369  breldmg 3407  elreldm 3425  relimasn 3517  asymref2 3532  funopg 3652  funssres 3657  fununi 3668  funimass2 3678  fneu 3698  fnun 3700  fss 3742  fco 3743  opelf 3747  f1oun 3815  f1dmex 3821  fv3 3844  funopfvg 3863  fvelima 3875  fvelimab 3876  fvco 3885  fvco2 3886  fvopab3ig 3889  elrnopabg 3914  dff3 3931  funfvima2 3967  funfvima3 3968  isorel 4008  isocnv 4010  isotr 4011  isotrALT 4012  isomin 4013  isoini 4014  isofrlem 4015  f1oweALT 4020  ndmoprcl 4105  1stdm 4169  onfununi 4209  onopriun 4211  tfrlem2 4213  tfrlem7 4218  tfrlem8 4219  tfrlem9 4220  tfrlem11 4222  tfr3 4227  rdglim 4249  tz7.49 4260  abianfp 4263  oevn0 4290  oaordi 4316  oawordeu 4325  oawordexr 4326  oalimcl 4330  oaass 4331  oarec 4332  omordi 4333  omcan 4336  omwordri 4339  omword1 4340  omlimcl 4345  odi 4346  omass 4347  oeordi 4350  oecan 4352  oewordi 4354  oewordri 4355  oeordsuc 4357  oeoa 4360  oeoe 4362  nnacom 4373  nnmcom 4381  oaabs 4392  omsmolem 4396  omsmo 4397  eceqopreq 4454  th3qlem1 4455  th3qlem2 4456  f1oen2g 4535  en3d 4542  dom2d 4545  fundmen 4569  undom 4579  xpdom2 4583  pw2en 4587  ac6sfilem3 4590  ac6sfi 4591  sbthlem1 4592  ensdomtr 4616  domsdomtr 4621  enen1 4622  enen2 4623  domen1 4624  domen2 4625  sdomen1 4626  sdomen2 4627  mapenlem2 4637  mapen 4638  mapdom2 4641  mapunen 4649  nneneq 4659  php 4660  php3 4662  finsucdom 4673  pssinf 4674  isfinite1 4677  infsdomnn 4678  pssnn 4681  ssfi 4683  domfi 4684  unblem3 4688  unfilem1 4694  unifi 4701  fiint 4703  abfii4 4707  fodomfi 4709  fodomfib 4710  iunfi 4712  pm54.43 4715  supmo 4719  suppr 4733  suc11reg 4750  inf3lem1 4758  inf3lem5 4762  unbnn3 4785  zfregs 4793  setind 4794  r1ord 4801  r1val1 4804  tz9.12lem3 4807  rankr1 4820  ssrankr1 4822  rankxplim3 4860  rankxpsuc 4861  aceq3 4879  aceq5lem4 4884  aceq5 4886  aceq6b 4888  ac6s 4902  numthlem 4929  zorn2lem1 4934  zorn2lem4 4937  zorn2lem5 4938  zorn2lem6 4939  zorn2lem7 4940  fodomb 4946  unidom 4954  uniimadom 4956  unxpdomlem 4993  cardlim 5001  ondomon 5006  carduni 5008  alephordi 5024  alephle 5034  cardaleph 5035  cardinfima 5041  alephval2 5052  alephval3 5053  cflim 5059  axrepndlem1 5098  axrepndlem2 5099  axrepnd 5100  axpowndlem4 5106  axinfndlem1 5111  axacndlem4 5116  axacndlem5 5117  axacnd 5118  mulclpi 5175  mulcanpi 5181  ltmpi 5185  indpi 5188  ltaddpq 5233  ltrpq 5239  elprpq 5249  prcdpq 5251  distrlem4pr 5284  psslinpr 5289  prlem934a 5291  prlem934 5293  ltaddpr 5294  ltexprlem3 5298  ltexprlem5 5300  ltaprlem 5304  prlem936 5309  suplem1pr 5315  mulcmpblnr 5337  recexsrlem 5366  mulgt0sr 5368  ssgt0sr 5371  suppsrlem 5375  suppsr2 5377  suppsr3 5378  suprelem 5413  axrrecex 5438  cnegexlem1 5499  cnegexlem2 5500  addcani 5505  renegcli 5570  mulgt0 5663  xrre 5723  xrre2 5724  addgegt0i 5754  msqgt0 5769  gt0ne0 5772  addgt0 5801  addgegt0 5802  addge0 5804  mulge0 5833  mulge0OLD 5834  recex 5840  mulcani 5842  recne0 5878  recid 5881  redivcli 5938  prodgt0i 5959  prodge0i 5960  prodgt0 5966  prodgt02 5967  prodge0 5968  prodge02 5969  lemul1OLD 5974  ltmul12a 5985  lemul12aOLD 5987  mulgt1 5989  ltdiv1OLD 5994  lediv1OLD 5996  ltmuldivOLD 6008  ltmuldiv2OLD 6010  ltdivmulOLD 6012  ledivmulOLD 6014  lemuldiv2OLD 6022  ltrec 6029  lerec 6030  lt2msq 6031  lediv12a 6041  le2msq 6048  ledivp1 6050  ledivp1i 6051  ltdivp1i 6052  lt1nnn 6092  nnleltp1 6100  nndivtr 6106  rpmulcl 6207  rpneg 6211  lble 6215  sup2 6219  suprub 6224  suprlub 6225  suprnub 6226  suprleub 6227  infmrcl 6237  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxr 6249  supxrre 6251  supxrunb1 6257  supxrunb2 6258  supxrbnd 6259  supxrub 6266  supxrleub 6267  dfn2 6280  lt0nnn0 6284  nnnn0addcl 6293  elnnz 6313  elnnz1 6323  nn0sub 6329  zaddcl 6333  zmulcl 6348  zltp1le 6349  btwnnz 6363  zneo 6371  uzind2 6377  uzindOLD 6379  uzwo4OLD 6381  nn0ind-raph 6385  zindd 6386  zbtwnre 6393  qaddcl 6408  qmulcl 6410  qreccl 6412  qbtwnre 6418  qsqueeze 6420  monoord 6482  iooss1 6499  iooss2 6500  elioo4g 6511  iccsupr 6525  icoshft 6535  icounlem 6539  icoun 6540  ioojoin 6543  eluz 6553  uz11 6559  eluzp1m1 6560  uzwo 6582  uzwoOLD 6583  elfzel2g 6608  fzen 6622  elfz2nn0 6625  elfz3nn0 6627  fznn0sub 6628  fsequb 6654  fsequb2 6655  fseqsupcl 6656  fseqsupubi 6657  seq1rn2 6686  ser1add2i 6703  ser1addi 6704  seqzfveq 6749  seqzrn2 6751  expp1 6769  expordi 6797  expcan 6798  expord 6799  expword2i 6802  exple1 6804  expubnd 6805  sq11 6826  sq01 6848  expnbnd 6852  expnlbnd 6853  expnlbnd2 6854  sqr0 6873  sqrlem12 6885  sqrcl 6911  sqrgt0 6912  sqrge0 6913  sqrle 6914  sqr00 6915  sqrsq 6923  sqsqr 6924  crulem 6937  replim 6962  absrpcl 7057  absid 7064  absnid 7065  leabs 7066  abssubne0 7085  absmax 7100  seq1bndi 7113  cau2i 7116  caubndi 7129  faclbnd 7148  faclbnd4lem4 7154  bccl2 7174  climcl 7181  sumeq2 7188  fsum1s 7212  fsum1s2 7213  fsump1s 7216  fsumcllem 7217  fsum1ps 7221  fsumsplit 7223  fsumadd 7225  fsumcom 7231  fsumrev 7232  fsumshftm 7235  fsummulc1 7236  fsummulc2 7237  fsumdivc 7238  fsumdivcALT 7239  fsumconst 7241  fsumcmp 7243  fsumcmpndx2 7245  fsumabs 7246  clm3i 7282  clm4lei 7284  clm0i 7286  clm0nnsi 7288  clmi2a 7294  climconsti 7297  climunii 7301  2climnn 7305  2climnn0 7306  climshfti 7307  iserzshft2i 7310  climge0 7315  climabs0i 7316  climaddc1 7321  climaddc2 7322  climmullem4 7326  climmullem5 7327  climmulc2 7332  climsubc2 7334  clim2serz 7337  climcmplem 7340  climserzlei 7350  climcaui 7359  caucvglem2 7361  caucvglem6 7365  caucvgi 7366  serzf0i 7372  ser1cmp2i 7380  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  cvgcmp3ce 7394  isumclim2f 7402  isumcl 7413  iserzgt0 7415  isumcmpii 7419  reccnv 7422  infcvglem3 7427  expcnv 7437  georeclim 7445  geoisumr 7448  cvgratlem2ALT 7453  cvgratlem3ALT 7454  cvgratlem1 7455  cvgratlem2 7456  cvgratlem3 7457  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag3 7465  fsum0diag4 7466  elcncf 7470  elcncf1di 7475  ivthlem9 7494  efaddlem23 7565  eftlex 7583  reeff1o 7634  efieq1re 7694  xpnnen 7711  znnen 7714  unbenlem 7716  infpnlem1 7718  infxpidmlem7 7770  infxpidmlem10 7773  infxpidmlem11 7774  alephexp1 7796  uniopn 7810  tgcl 7836  tgss2 7849  basgen2 7851  subbas2 7857  subtop 7858  cctop 7862  retopbas 7865  ntrval 7886  iincld 7889  clsval2 7895  0ntr 7912  elcls 7914  elcls3 7921  neii1 7931  neii2 7932  0nnei 7936  islp2 7957  clslp 7958  qdensere 7961  cnima 7977  cnclima 7981  cnsscnp 7982  cncnplem4 7987  metxplem3 8038  metxplem4 8043  metxp 8044  rnblssm 8061  blss 8063  ssbl 8065  opnuni 8078  opnin 8079  rnblopn 8084  metequiv 8091  metcnp 8098  metcn 8100  metcnpi3 8103  metcnpi4 8104  metcni2 8106  metcnss2 8110  metdnsconst 8112  cncfmet 8116  lmnn 8146  caun0 8156  lmsslem 8163  caussi 8165  metelcls 8176  metcnp4 8181  metcn4i 8183  xplmi 8184  xpcn 8187  iscms2lem3 8202  iscms2lem4 8203  iscms2lem5 8204  lmcau 8207  cmsss 8208  bcthlem2 8211  bcthlem10 8219  bcthlem21 8230  bcthlem25 8234  bcthlem28 8237  bcthlem33 8242  bcth 8243  grpass 8260  grpidinvlem3 8263  grpidinvlem4 8264  grpid 8282  grpasscan1 8294  grpnnncan2 8311  gxnval 8316  gxnn0suc 8320  gxid 8329  gxadd 8331  gxmul 8334  grplactf1o 8339  subgabl 8365  ghgrpilem2 8375  nvz 8544  nvcni 8576  nvcni2 8577  nvcni3 8578  nvlmle 8580  vacnlem3 8584  vacnlem4 8585  sspmval 8646  sspival 8651  sspimsval 8653  nmoub3i 8690  nmobndseqi 8695  nmlno0lem 8708  nmlnoubi 8711  lnon0 8713  nmblolbi 8715  isblo3i 8716  blocni 8720  ipasslem1 8746  ipasslem5 8750  ipdir 8758  ipass 8761  ipsubdir 8764  sspph 8771  ubthlem5 8791  ubthlem14 8802  ubthi 8804  htthlem7 8888  htthlem10 8891  htthlem12 8893  psref 8911  spwmo 8918  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  sineq0re 8985  efifolem2 8995  shftefif1olem 9013  eff1i 9016  normpyc 9289  shel 9356  shsubclOLD 9366  chel 9376  hlimcauii 9382  ocorth 9440  shorth 9444  ocnel 9446  occli 9457  projlem13 9474  projlem15 9476  projlem26 9487  projlem27 9488  projlem28 9489  pjthlem13 9507  pjtheu 9512  pjpj0i 9531  pjoml 9545  shscli 9557  shsel1 9561  chintcli 9571  shlej1 9631  shmodsi 9638  shmodi 9639  h1dn0 9751  spansni 9756  spansnmul 9763  spansnss 9770  elspansn4 9772  h1datomi 9780  cm2j 9839  osumlem4 9859  osumlem6 9861  spansncvi 9875  5oalem6 9882  pjige0 9914  pjsumi 9933  pjdsi 9935  pjds3i 9936  homco1 10007  homulass 10008  eigre 10041  eigorth 10044  nmopub2tALT 10113  nmfnleub2 10130  elnlfn2 10133  kbpj 10160  homco2 10180  nmlnop0iALT 10199  nmopun 10218  nmbdoplb 10229  nmcopexlem1 10230  nmcopexlem6 10235  nmcoplb 10239  nmcfnexlem1 10259  nmcfnexlem6 10264  nmcfnlb 10268  nlelchi 10273  branmfn 10317  branmfnOLD 10318  bra11 10321  cnvbraval 10323  leopadd 10345  leopmuli 10346  leopmul2i 10348  leoptr 10350  pjnmopi 10355  pjnormssi 10376  pjclem4 10408  pj3si 10416  hstel2 10427  hst1h 10435  stlei 10448  stlesi 10449  staddi 10454  stadd3i 10456  strlem3a 10460  hstrlem3a 10468  stcltrlem1 10484  spansncv2 10501  mdslmd1lem3 10535  mdslmd1lem4 10536  csmdsymi 10542  mdexchi 10543  atss 10554  atsseq 10555  superpos 10562  chcv1 10563  chjatom 10565  hatomic 10568  hatomistici 10570  cvbr3i 10575  atcv1 10589  atexch 10590  atomli 10591  atoml2i 10592  atcvatlem 10594  atcvati 10595  atcvat2i 10596  irredlem3 10601  irredlem4 10602  atcvat3i 10605  atcvat4i 10606  mdsymlem3 10614  sumdmdii 10624  sumdmdlem 10627  dmdbr5ati 10631  cdj1i 10642  cdj3lem1 10643  cdj3lem2b 10646  ghomgsg 10680  ghomf1olem 10681  findabrcl 10703  ee7.2a 10710  uninqs 10730  infi1 10735  ficli 10756  f2imacnv 10758  oooeqim2 10759  domrngref 10764  imgfldref2 10768  ref3w 10772  twpar2 10773  f1fi 10779  cpref 10782  inttr 10787  xrletr2 10790  njtlc 10804  restidsing 10805  twsymr 10808  prj1 10809  imfstnrelc 10810  unpde2eg22 10826  jidd 10840  midd 10841  infi 10854  inposet 10868  pospos 10882  tostos 10883  toplat 10884  exidu1 10902  ismnd1 10927  unmnd 10951  fora2 10953  uridm 10956  on1el4 10963  fldi 10974  cdrci 10994  truni1 10999  truni3 11001  hmeomap 11024  hmeocna 11025  hmeocnb 11026  cmphmp 11027  cnvhmpha 11031  cnvhmphb 11032  hmphre 11036  hmphtr 11037  hmeogrp 11044  homcard 11045  hmeobc 11048  top2ind 11050  homindlem2 11052  fipfil2 11077  fgsb 11082  efilcp 11083  fgsb2 11086  efilcp2 11087  cnfilca 11088  rcfpfillem4 11092  limfillem2 11102  stfincomp 11122  bwt2 11123  usinuniop 11128  topsinind 11136  altretop 11144  iintlem1 11155  trnij 11160  idosd 11198  rdmob 11202  cmpasso 11227  cmpassoh 11256  homgrf 11257  imonclem 11268  ismonc 11269  cmpmon 11270  icmpmon 11271  idmon 11272  iepiclem 11278  isepic 11279  fmp 11294  obsubc2 11304  idsubc 11305  domsubc 11306  codsubc 11307  cmpsubc 11310  imp5a 11342  imp5g 11344  expr 11361  imp5q 11384  eqeu 11394  lpni 11417  finminlem 11418  ordiso 11426  ordtypelem4 11430  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  hartog 11436  omsubsuc2 11439  omsubsdomlem2 11441  omsubsdom 11442  omsubel 11444  omsubindss 11449  infenomsub 11450  clsint2 11466  opnnei 11469  hausnei2 11471  cnpnei 11472  cncls 11473  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  cncomp 11494  alexsublem2 11497  alexsublem4 11499  alexsub 11500  dfcon2 11501  connsub 11502  cnconn 11503  subtopmetlem 11505  subtopmet 11506  reconnlem1 11507  reconnlem5 11511  iccconn 11514  ivthALT 11515  topfneec 11562  ptfinfin 11569  lfinpfin 11574  locfincomp 11575  comppfsc 11578  neibastop3 11585  topmtcl 11586  topjoin 11588  fnejoin1 11591  fnejoin2 11592  t0dist 11602  ist1-3 11604  t1sncld 11606  t1sep 11607  regsep 11611  nrmsep 11615  nrmsep2 11616  fbssint 11626  fsubbas 11630  fgfil 11638  fbfgss 11640  filrn 11643  supfil 11645  filfinnfr 11646  isufil2 11650  ufilss 11652  ufprim 11654  filssufillem 11655  filssufil 11656  ufileulem 11657  ufileu 11658  uffixfr 11660  ufilen 11664  flimopn 11679  limfilcf 11683  flimcls 11684  hausfillim 11685  cnpfillim 11686  elfilmap 11690  elfilmap2 11691  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem4 11703  fmfnfm 11704  flimfbas 11713  fclusneii 11721  fclusbas 11722  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscnp 11730  isfclusf 11737  dirtr 11753  tosdir 11755  tailfb 11762  filnetlem5 11767  gapmlem 11783  gapm 11784  morex 11804  dif1card 11835  findcard 11836  fimax 11837  fixp 11840  ac6gf 11841  indexa 11845  indexd 11846  indexf 11847  fipreima 11848  inficl 11849  supclt 11854  supubt 11855  fimaxre 11856  filbcmb 11857  add20 11858  eluzadd 11860  fzm1 11867  rddif 11869  absrdbnd 11870  sdclem1 11875  sdclem2 11876  sdc 11877  nnubfi 11881  nninfnub 11882  fsum00 11883  fsumlt 11884  fsumltisum 11887  fsumleisum 11890  fsumlt1 11894  fiinbas 11905  metf1o 11907  metsstop 11909  blhalf 11911  mettrifi 11912  mettrifi2 11913  geomcau 11914  lmclim2 11915  metdcn 11918  iccsplit 11919  icoopnst 11940  iocopnst 11941  lincmb01icc 11943  cncfco 11948  cnres 11950  paste 11954  hmeoopn 11960  hmeocld 11961  lmtlm 11969  tx1cn 11976  tx2cn 11977  uptx 11978  txcnopab 11980  txcnoprab 11981  txsubsp 11983  txcld 11985  sstotbnd 11992  totbndss 11993  isbnd3 11997  bndss 11998  totbndbnd 12000  ismtyhmeolem 12006  ismtybndlem 12008  ismtyres 12010  heiborlem1 12011  heiborlem11 12021  heiborlem13 12023  heiborlem15 12025  heiborlem16 12026  heiborlem23 12033  heiborlem27 12037  heiborlem29 12039  heiborlem31 12041  heiborlem32 12042  heiborlem35 12045  heiborlem36 12046  rrndstprj2 12074  rrncms 12075  rrntotbndlem1 12076  rrntotbnd 12078  reheibor 12081  iccbnd 12082  phtpyval 12089

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 145  df-an 223

Copyright terms: Public domain