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 497  3imtr3g 552  ordi 596  jcad 600  orcanai 690  mpanl1 706  mpanl2 707  mpanr1 709  mpanr2 710  mpanlr1 711  pm4.82 739  3adantl1 803  3adantl2 804  3adantl3 805  3jcad 820  3expia 835  3an1rs 845  3imp1 846  3imp2 848  syl3anl1 873  syl3anl2 874  syl3anl3 875  3anidm12 882  3anidm23 884  3jaoian 889  3jaodan 890  mp3anl1 910  mp3anl2 911  mp3anl3 912  19.21ad 1059  19.26 1067  equtr2 1133  equs4 1150  dvelimfALT 1153  a4imt 1158  a4imed 1161  equvini 1168  equs5a 1197  ax11v2 1215  ax11b 1220  dfsb2 1225  hbsb4 1248  dvelimdf 1251  sbcom 1258  equvin 1275  dvelimALT 1353  ax11eq 1363  ax11el 1364  ax11indi 1367  ax11indalem 1368  ax11inda2ALT 1369  ax11inda 1371  a12stdy2 1373  a12lem1 1376  mopick 1433  moexex 1438  nelneq 1561  nelneq2 1562  r19.21advv 1721  r19.21bi 1725  r19.23ai 1742  r19.23advv 1749  r19.15 1753  rcla4va 1875  reu3 1931  ra4sbca 1998  ra4esbca 1999  csbexg 2008  ra4csbela 2042  ssel2 2064  sstr 2072  sspsstr 2151  psssstr 2152  neldif 2165  reuss2 2275  reupick 2279  ssne0 2305  ssdisj 2318  disjpss 2319  disjssun 2326  pssdifn0 2329  dedth2h 2387  dedth4h 2389  sspr 2475  prel12 2484  iineq2 2579  ssiun 2592  dtruALT 2748  pwssun 2827  poirr 2845  potr 2846  reuuni2f 2883  mouniss 2890  elpwunsn 2912  frirr 2924  wefrc 2943  wereu 2945  ordelss 2964  trssord 2965  nordeq 2967  ordelord 2970  tz7.7 2973  ordsseleq 2976  onfr 2986  ordtr2 3002  oninton 3012  oneqmini 3017  limelon 3032  trsuc 3055  ordsssuc2 3059  unizlim 3113  limuni3 3123  tfi 3126  limomss 3137  ordom 3141  peano5 3153  findsg 3157  tfinds 3161  tfindsg 3162  tfindsg2 3163  brrelex 3207  optocl 3235  elrel 3253  relop 3275  opelxpex2 3279  breldmg 3316  elreldm 3338  relimasn 3425  asymref2 3440  funopg 3547  funssres 3552  fununi 3563  funimass2 3573  fneu 3592  fnun 3594  fss 3635  fco 3636  opelf 3640  f1oun 3706  f1dmex 3710  fv3 3733  funopfvg 3752  fvelima 3764  fvelimab 3765  fvco 3774  fvco2 3775  fvopab3ig 3778  elrnopabg 3800  dff2 3817  funfvima2 3853  funfvima3 3854  isorel 3894  isocnv 3896  isotr 3897  isotrALT 3898  isomin 3899  isoini 3900  isofrlem 3901  f1oweALT 3906  tfrlem2 3912  tfrlem7 3917  tfrlem8 3918  tfrlem9 3919  tfrlem11 3921  tfr3 3926  rdglimt 3948  tz7.49 3959  abianfp 3962  ndmoprcl 4044  1stdm 4109  oevn0 4154  oaordi 4180  oawordeu 4189  oawordexr 4190  oalimcl 4194  oaass 4195  oarec 4196  omordi 4197  omcan 4200  omwordri 4203  omword1 4204  omlimcl 4209  odi 4210  omass 4211  oeordi 4214  oecan 4216  oewordi 4218  oewordri 4219  oeordsuc 4221  nnacom 4233  nnmcom 4241  oaabs 4252  omsmolem 4256  omsmo 4257  ecoptocl 4303  eceqopreq 4313  th3qlem1 4314  th3qlem2 4315  f1oen2g 4394  en3d 4401  dom2d 4404  fundmen 4428  undom 4438  xpdom2 4442  pw2en 4446  sbthlem1 4447  ensdomtr 4471  domsdomtr 4476  enen1 4477  enen2 4478  domen1 4479  domen2 4480  sdomen1 4481  sdomen2 4482  fodomr 4483  mapenlem2 4490  mapen 4491  mapdom2 4494  mapunen 4502  nneneq 4512  php 4513  php3 4515  php3OLD 4516  finsucdomOLD 4527  pssinfOLD 4528  isfinite1OLD 4531  infsdomnn 4532  pssnn 4534  ssfi 4537  ssfiOLD 4538  domfiOLD 4539  unblem3 4542  isfinite2OLD 4546  unfilem1 4548  unifiOLD 4557  fiint 4559  fiintOLD 4560  abfii4OLD 4564  fodomfiOLD 4566  fodomfibOLD 4567  pm54.43 4572  supmo 4576  supnub 4582  suppr 4590  suc11reg 4605  inf3lem1 4613  inf3lem5 4617  inf3lem6 4618  unbnnt 4639  zfregs 4647  setind 4648  r1ord 4655  r1val1 4658  tz9.12lem3 4661  rankr1 4674  ssrankr1 4676  rankxplim3 4714  rankxpsuc 4715  aceq3 4733  aceq5lem4 4738  aceq5 4740  aceq6b 4742  ac6s 4756  numthlem 4783  zorn2lem1 4788  zorn2lem4 4791  zorn2lem5 4792  zorn2lem6 4793  zorn2lem7 4794  fodomb 4800  unidom 4808  uniimadom 4810  sucdom 4842  unxpdomlem 4843  cardlim 4851  ondomon 4856  carduni 4858  alephordi 4874  alephle 4884  cardaleph 4885  cardinfima 4891  alephval2 4902  alephval3 4903  cflim 4909  axrepndlem1 4944  axrepndlem2 4945  axrepnd 4946  axpowndlem4 4952  axinfndlem1 4957  axacndlem4 4962  axacndlem5 4963  axacnd 4964  mulclpi 5021  mulcanpi 5027  ltmpi 5031  indpi 5034  ltaddpq 5079  ltrpq 5085  elprpq 5095  prcdpq 5097  distrlem4pr 5130  psslinpr 5135  prlem934a 5137  prlem934 5139  ltaddpr 5140  ltexprlem3 5144  ltexprlem5 5146  ltaprlem 5150  prlem936 5155  suplem1pr 5161  mulcmpblnr 5183  recexsrlem 5212  mulgt0sr 5214  ssgt0sr 5217  suppsrlem 5221  suppsr2 5223  suppsr3 5224  suprelem 5259  axrrecex 5284  cnegextlem1 5345  cnegextlem2 5346  addcan 5351  renegcl 5416  letrt 5525  xrletrt 5564  xrret 5569  xrre2t 5570  addgegt0 5600  msqgt0t 5615  gt0ne0t 5618  addgt0t 5647  addgegt0t 5648  addge0t 5650  mulge0t 5679  recext 5684  mulcan 5686  mulcanOLD 5687  mulcan2tOLD 5693  divmult 5707  recne0t 5732  recidt 5735  div23t 5742  div13t 5743  div12t 5744  divdirtOLD 5751  divmuldivt 5780  divadddivt 5784  divdivdivt 5785  redivcl 5798  prodgt0 5819  prodge0 5820  prodgt0t 5826  prodgt02t 5827  prodge0t 5828  prodge02t 5829  ltmul1t 5830  ltmul12it 5841  lemul12itOLD 5843  mulgt1t 5845  ltdiv1tOLD 5850  lediv1tOLD 5852  ltmuldivtOLD 5864  ltmuldiv2tOLD 5866  ltdivmultOLD 5868  ledivmultOLD 5869  lemuldiv2tOLD 5877  ltrect 5884  lerect 5885  lt2msqt 5886  lediv12it 5896  le2msqt 5903  ledivp1t 5905  ledivp1 5906  ltdivp1 5907  lt1nnn 5947  nnleltp1t 5954  nndivtrt 5960  lble 6047  sup2 6051  suprub 6056  suprlub 6057  suprnub 6058  suprleub 6059  infmrcl 6069  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxr 6081  supxrre 6083  supxrun 6085  supxrunb1 6089  supxrunb2 6090  supxrbnd 6091  supxrub 6098  supxrleub 6099  dfn2 6112  lt0nnn0 6116  nnnn0addclt 6125  elnnz 6145  elnnz1 6155  nn0subt 6161  zaddclt 6165  zmulclt 6180  zltp1let 6181  btwnnzt 6192  zneo 6200  uzind2 6206  uzindOLD 6208  uzwo4OLD 6210  nn0ind-raph 6214  zbtwnre 6221  qaddclt 6269  qmulclt 6271  qrecclt 6273  qbtwnre 6278  qsqueeze 6280  rpmulclt 6291  monoord 6294  seq1rn2 6321  ser1add2 6338  ser1add 6339  iooss1 6373  iooss2 6374  elioo4g 6385  iccsupr 6398  icoshft 6408  icounlem 6412  icoun 6413  ioojoint 6416  eluzt 6426  uz11t 6432  eluzp1m1t 6433  uzwo 6455  uzwoOLD 6456  elfzel2g 6480  elfz2nn0t 6495  elfz3nn0t 6497  fznn0subt 6498  fsequb 6523  fsequb2 6524  fseqsupcl 6525  fseqsupub 6526  seqzfveq 6554  seqzrn2 6556  expp1t 6574  expordit 6600  expcant 6601  expordt 6602  expword2it 6605  exple1t 6607  expubndt 6608  sq11t 6629  sq01t 6651  expnbndt 6654  expnlbndt 6655  sqr0 6672  sqrlem12 6684  sqrclt 6710  sqrgt0t 6711  sqrge0t 6712  sqrlet 6713  sqr00t 6714  sqrsqt 6722  sqsqrt 6723  crulem 6736  replimt 6761  absrpclt 6855  absidt 6862  absnidt 6863  leabst 6864  abssubne0t 6882  absmaxt 6897  seq1bnd 6910  cau2 6913  cau5i 6917  cvg3 6923  caubnd 6926  faclbnd 6945  faclbnd4lem4 6951  bccl2t 6971  climcl 6978  sumeq2 6985  fsum1s 7009  fsum1s2 7010  fsump1s 7013  fsumcllem 7014  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsumshftm 7032  fsummulc1 7033  fsummulc2 7034  fsumdivc 7035  fsumdivcALT 7036  fsumconst 7038  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  clm3 7079  clm4le 7081  clm0 7083  clm0nns 7085  clmi2at 7091  climconst 7094  climunii 7098  2climnn 7102  2climnn0 7103  climshft 7104  iserzshft2 7107  climge0 7112  climabs0 7113  climaddc1 7118  climaddc2 7119  climmullem4 7123  climmullem5 7124  climmulc2 7129  climsubc2 7131  clim2serzt 7134  climcmplem 7137  climserzle 7147  climcau 7156  caucvglem2 7158  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  ser1cmp2 7177  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  cvgcmp3cet 7190  isumclim2tf 7198  isumclt 7209  iserzgt0 7211  isumcmpi 7215  reccnv 7218  infcvglem3 7223  expcnv 7233  georeclim 7240  geoisumr 7243  cvgratlem2ALT 7248  cvgratlem3ALT 7249  cvgratlem1 7250  cvgratlem2 7251  cvgratlem3 7252  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag3 7260  fsum0diag4 7261  elcncf 7265  elcncf1d 7270  ivthlem9 7289  efaddlem23 7360  eftlext 7378  reeff1o 7426  xpnnen 7499  znnen 7502  unbenlem 7504  infpnlem1 7506  infxpidmlem7 7558  infxpidmlem10 7561  infxpidmlem11 7562  infmap2lem1 7579  alephexp1 7584  uniopnt 7598  tgclt 7624  tgss2t 7637  basgen2t 7639  subbas2OLD 7645  subtop 7646  fctopOLD 7650  cctop 7652  retopbas 7655  ntrval 7676  iincld 7679  clsval2 7685  0ntr 7702  elcls 7704  elcls3 7711  neii1 7721  neii2 7722  0nnei 7726  islp2 7747  clslp 7748  qdensere 7751  cnima 7767  cnclima 7771  cnsscnp 7772  cncnplem4 7777  cncnp 7778  metxplem3 7828  metxplem4 7833  metxp 7834  rnblssm 7851  blss 7853  ssbl 7855  opnuni 7868  opnin 7869  rnblopn 7874  metcnp 7887  metcn 7889  metcnpi3 7892  metcnpi4 7893  metcni2 7895  metcnss2 7899  metdnsconst 7901  cncfmet 7905  lmnn 7935  caun0 7945  lmsslem 7952  caussi 7954  metelcls 7965  metcnp4 7970  metcn4i 7972  xplmi 7973  xplm 7975  xpcn 7976  iscms2lem3 7991  iscms2lem4 7992  iscms2lem5 7993  lmcau 7996  cmsss 7997  bcthlem2 8000  bcthlem10 8008  bcthlem21 8019  bcthlem25 8023  bcthlem28 8026  bcthlem33 8031  bcth 8032  grpass 8047  grpidinvlem3 8050  grpidinvlem4 8051  grpid 8065  grpasscan1 8077  grpnnncan2 8093  grplactf1o 8098  subgabl 8123  ghgrpilem2 8134  nvz 8297  nvcni 8329  nvcni2 8330  nvcni3 8331  nvlmle 8333  sspmval 8392  sspival 8397  sspimsval 8399  nmoub3i 8436  nmobndseqi 8440  nmlno0lem 8453  nmlnoubi 8456  lnon0 8458  nmblolbi 8460  isblo3i 8461  blocni 8465  ipasslem1 8490  ipasslem5 8494  ipdir 8502  ipass 8505  ipsubdir 8508  sspph 8515  ubthlem5 8533  ubthlem14 8542  ubthi 8544  htthlem7 8626  htthlem10 8629  htthlem12 8631  psref 8649  spwmo 8656  spwpr4OLD 8663  spwpr4aOLD 8664  efifolem2 8723  shftefif1olem 8741  eff1i 8744  normpyct 9013  shelt 9080  shsubcltOLD 9090  chelt 9100  hlimcaui 9106  ocorth 9164  shorth 9168  ocnelt 9170  occl 9181  projlem13 9198  projlem15 9200  projlem26 9211  projlem27 9212  projlem28 9213  pjthlem13 9231  pjtheut 9236  pjpj0 9255  pjomlt 9269  shscl 9281  shsel1t 9285  chintcl 9295  shlej1t 9355  shmods 9362  shmod 9363  h1dn0 9475  spansn 9480  spansnmul 9487  spansnsst 9494  elspansn4t 9496  h1datom 9504  cm2jt 9563  osumlem4 9581  osumlem6 9583  spansncv 9597  5oalem6 9604  pjige0t 9636  pjsumt 9655  pjds 9657  pjds3 9658  homco1t 9727  homulasst 9728  eigret 9761  eigortht 9764  nmopub2tALT 9833  nmfnleub2t 9850  elnlfn2t 9853  kbpjt 9880  homco2t 9901  nmlnop0ALT 9920  nmopunt 9939  nmbdoplbt 9950  nmcopexlem1 9951  nmcopexlem6 9956  nmcoplbt 9960  nmcfnexlem1 9980  nmcfnexlem6 9985  nmcfnlbt 9989  nlelch 9994  branmfnt 10038  bra11 10041  cnvbravalt 10043  leopaddt 10065  leopmulit 10066  leopmul2it 10068  leoptrt 10070  pjnmop 10075  pjnormss 10096  pjclem4 10127  pj3s 10135  hstel2t 10146  hst1ht 10154  stle 10167  stles 10168  stadd 10173  stadd3 10175  strlem3a 10179  hstrlem3a 10187  stcltrlem1 10203  spansncv2t 10220  mdslmd1lem3 10254  mdslmd1lem4 10255  csmdsym 10261  mdexch 10262  atss 10273  atsseq 10274  superpos 10281  chcv1t 10282  chjatom 10284  hatomict 10287  hatomistic 10289  cvbr3 10294  atcv1t 10307  atexcht 10308  atoml 10309  atoml2 10310  atcvatlem 10312  atcvat 10313  atcvat2 10314  irredlem3 10319  irredlem4 10320  atcvat3 10323  atcvat4 10324  mdsymlem3 10332  sumdmdi 10342  sumdmdlem 10345  sumdmdlem2 10346  dmdbr5at 10349  cdj1 10360  cdj3lem1 10361  cdj3lem2b 10364  ghomgsg 10395  ghomf1olem 10396  findabrcl 10418  ee7.2a 10425  uninqs 10441  infi1 10447  infi1OLD 10448  ficli 10472  ficliOLD 10473  f2imacnv 10475  oooeqim2 10476  cdrci 10494  truni1 10499  esnnei 10508  hmeomap 10518  hmeocna 10519  hmeocnb 10520  cmphmp 10521  cnvhmpha 10525  cnvhmphb 10526  hmphre 10530  hmphtr 10531  hmeogrp 10538  homcard 10539  hmeobc 10542  sfseqeq 10543  top2ind 10548  homindlem2 10550  qusp 10555  filint 10562  fipfil2 10564  fipfil2OLD 10565  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  infi 10578  infiOLD 10579  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem4 10591  rcfpfillem4OLD 10592  sfvlim 10605  limfillem2OLD 10608  iintlem1 10632  trnij 10637  idosd 10677  rdmob 10681  cmpasso 10706  cmpassoh 10729  homgrf 10730  imonclem 10741  ismonc 10742  cmpmon 10743  icmpmon 10744  idmon 10745

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