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 687  mpanl1 703  mpanl2 704  mpanr1 706  mpanr2 707  mpanlr1 708  pm4.82 736  3adantl1 800  3adantl2 801  3adantl3 802  3jcad 817  3expia 832  3an1rs 842  3imp1 843  3imp2 845  syl3anl1 869  syl3anl2 870  syl3anl3 871  3anidm12 878  3anidm23 880  3jaoian 885  3jaodan 886  mp3anl1 906  mp3anl2 907  mp3anl3 908  19.21ad 1035  19.26 1043  equtr2 1120  equs4 1133  dvelimfALT 1136  a4at 1141  a4c1 1144  equvini 1151  equs5a 1181  ax11v2 1199  ax11b 1204  dfsb2 1209  hbsb4 1232  dvelimdf 1235  sbcom 1242  equvin 1257  ax11eq 1340  ax11el 1341  ax11indi 1344  ax11indalem 1345  ax11inda2ALT 1346  ax11inda 1348  a12stdy2 1350  a12lem1 1353  mopick 1410  moexex 1415  nelneq 1537  nelneq2 1538  r19.21advv 1697  r19.21bi 1701  r19.23ai 1718  r19.23advv 1725  r19.15 1729  rcla4va 1848  reu3 1902  ra4sbca 1969  ra4esbca 1970  csbexg 1979  ra4csbela 2013  ssel2 2035  sstr 2043  sspsstr 2122  psssstr 2123  neldif 2136  reuss2 2246  reupick 2250  ssne0 2276  ssdisj 2289  disjpss 2290  disjssun 2297  pssdifn0 2300  dedth2h 2358  dedth4h 2360  sspr 2445  prel12 2454  iineq2 2547  ssiun 2560  dtruALT 2716  pwssun 2789  poirr 2809  potr 2810  reuuni2f 2846  mouniss 2853  elpwunsn 2875  frirr 2887  wefrc 2906  wereu 2908  ordelss 2927  trssord 2928  nordeq 2930  ordelord 2933  tz7.7 2936  ordsseleq 2939  onfr 2949  ordtr2 2965  oninton 2975  oneqmini 2980  limelon 2995  trsuc 3018  ordsssuc2 3022  unizlim 3076  limuni3 3086  tfi 3089  limomss 3100  ordom 3104  peano5 3116  findsg 3120  tfinds 3124  tfindsg 3125  tfindsg2 3126  brrelex 3169  optocl 3197  elrel 3215  breldmg 3273  elreldm 3297  relimasn 3376  funssres 3492  fununi 3503  funimass2 3513  fneu 3532  fnun 3534  fss 3574  fco 3575  opelf 3579  f1oun 3645  f1dmex 3649  fv3 3672  funopfvg 3691  fvelima 3703  fvelimab 3704  fvco 3713  fvco2 3714  fvopab3ig 3717  elrnopabg 3739  dff2 3756  funfvima2 3792  funfvima3 3793  isorel 3833  isocnv 3835  isotr 3836  isotrALT 3837  isomin 3838  isoini 3839  isofrlem 3840  f1oweALT 3845  tfrlem2 3851  tfrlem7 3856  tfrlem8 3857  tfrlem9 3858  tfrlem11 3860  tfr3 3865  rdglimt 3887  tz7.49 3898  abianfp 3901  ndmoprgOLD 3983  ndmoprcl 3984  1stdm 4047  oevn0 4092  oaordi 4118  oawordeu 4127  oawordexr 4128  oalimcl 4132  oaass 4133  oarec 4134  omordi 4135  omcan 4138  omwordri 4141  omword1 4142  omlimcl 4147  odi 4148  omass 4149  oeordi 4152  oecan 4154  oewordi 4156  oewordri 4157  oeordsuc 4159  nnacom 4171  nnmcom 4179  oaabs 4190  omsmolem 4194  omsmo 4195  ecoptocl 4241  eceqopreq 4251  th3qlem1 4252  th3qlem2 4253  f1oen2g 4329  en3d 4336  dom2d 4339  fundmen 4363  undom 4372  xpdom2 4376  pw2en 4380  sbthlem1 4381  ensdomtr 4405  domsdomtr 4410  enen1 4411  enen2 4412  domen1 4413  domen2 4414  sdomen1 4415  sdomen2 4416  fodomr 4417  mapenlem2 4422  mapen 4423  mapdom2 4426  mapunen 4434  nneneq 4444  php 4445  php3 4447  finsucdom 4458  pssinf 4459  isfinite1 4462  infsdomnn 4463  pssnn 4465  ssfi 4467  domfi 4468  unblem3 4471  isfinite2 4475  unfilem1 4476  unifi 4484  fiint 4486  abfii4 4490  fodomfi 4492  fodomfib 4493  pm54.43 4498  supmo 4502  supnub 4508  suppr 4514  suc11reg 4529  inf3lem1 4537  inf3lem5 4541  inf3lem6 4542  unbnnt 4563  zfregs 4571  setind 4572  r1ord 4579  r1val1 4582  tz9.12lem3 4585  rankr1 4598  ssrankr1 4600  rankxplim3 4638  rankxpsuc 4639  aceq3 4657  aceq5lem4 4662  aceq5 4664  aceq6b 4666  ac6s 4680  numthlem 4707  zorn2lem1 4712  zorn2lem4 4715  zorn2lem5 4716  zorn2lem6 4717  zorn2lem7 4718  fodomb 4724  unidom 4732  uniimadom 4734  sucdom 4765  unxpdomlem 4766  cardlim 4774  ondomon 4779  carduni 4781  alephordi 4797  alephle 4807  cardaleph 4808  cardinfima 4814  alephval2 4825  alephval3 4826  cflim 4832  axrepndlem1 4867  axrepndlem2 4868  axrepnd 4869  axpowndlem4 4875  axinfndlem1 4880  axacndlem4 4885  axacndlem5 4886  axacnd 4887  mulclpi 4944  mulcanpi 4950  ltmpi 4954  indpi 4957  ltaddpq 5002  ltrpq 5008  elprpq 5018  prcdpq 5020  distrlem4pr 5053  psslinpr 5058  prlem934a 5060  prlem934 5062  ltaddpr 5063  ltexprlem3 5067  ltexprlem5 5069  ltaprlem 5073  prlem936 5078  suplem1pr 5084  mulcmpblnr 5106  recexsrlem 5135  mulgt0sr 5137  ssgt0sr 5140  suppsrlem 5144  suppsr2 5146  suppsr3 5147  suprelem 5182  axrrecex 5207  cnegextlem1 5268  cnegextlem2 5269  addcan 5274  renegcl 5339  letrt 5449  xrletrt 5488  xrret 5493  xrre2t 5494  addgegt0 5525  msqgt0t 5540  gt0ne0t 5543  addgt0t 5571  addgegt0t 5572  addge0t 5574  mulge0t 5603  recext 5608  mulcan 5610  mulcan2t 5613  divmult 5627  recne0t 5646  recidt 5649  div23t 5656  div13t 5657  div12t 5658  divdirt 5664  divmuldivt 5687  divadddivt 5691  divdivdivt 5692  redivcl 5705  prodgt0 5726  prodge0 5727  prodgt0t 5733  prodgt02t 5734  prodge0t 5735  prodge02t 5736  ltmul1t 5737  ltmul12it 5748  lemul12itOLD 5750  mulgt1t 5752  ltdiv1t 5756  lediv1t 5757  ltmuldivt 5768  ltmuldiv2t 5769  ltdivmult 5770  ledivmult 5771  lemuldiv2t 5776  ltrect 5783  lerect 5784  lt2msqt 5785  lediv12it 5795  le2msqt 5802  ledivp1t 5804  ledivp1 5805  ltdivp1 5806  lt1nnn 5846  nnleltp1t 5852  nndivtrt 5858  lble 5945  sup2 5949  suprub 5954  suprlub 5955  suprnub 5956  suprleub 5957  infmrcl 5967  xrsupsslem 5974  xrinfmsslem 5975  xrub 5978  supxr 5979  supxrre 5981  supxrun 5983  supxrunb1 5987  supxrunb2 5988  supxrbnd 5989  supxrub 5996  supxrleub 5997  dfn2 6010  lt0nnn0 6014  nnnn0addclt 6023  elnnz 6043  elnnz1 6053  nn0subt 6059  zaddclt 6063  zmulclt 6078  zltp1let 6079  btwnnzt 6090  zneo 6098  zneoOLD 6099  uzind2 6105  uzindOLD 6107  uzwo4OLD 6109  nn0ind-raph 6113  zbtwnre 6120  qaddclt 6158  qmulclt 6160  qrecclt 6162  qbtwnre 6167  qsqueeze 6169  rpmulclt 6179  monoord 6182  seq1rn2 6209  ser1add2 6226  ser1add 6227  iooss1 6261  iooss2 6262  elioo4g 6269  iccsupr 6282  icoshft 6292  icounlem 6296  icoun 6297  eluzt 6309  uz11t 6315  eluzp1m1t 6316  uzwo 6338  uzwoOLD 6339  elfzel2g 6363  elfz2nn0t 6378  elfz3nn0t 6380  fznn0subt 6381  fsequb 6406  fsequb2 6407  fseqsupcl 6408  fseqsupub 6409  seqzfveq 6437  seqzrn2 6439  expp1t 6457  expordit 6482  expcant 6483  expordt 6484  expword2it 6487  exple1t 6489  expubndt 6490  sq11t 6511  sq01t 6533  expnbndt 6536  sqr0 6553  sqrlem12 6565  sqrclt 6591  sqrgt0t 6592  sqrge0t 6593  sqrlet 6594  sqr00t 6595  sqrsqt 6603  sqsqrt 6604  crulem 6617  replimt 6643  absrpclt 6741  absidt 6748  absnidt 6749  leabst 6750  abssubne0t 6771  seq1bnd 6798  cau2 6801  cau5i 6805  cvg3 6811  caubnd 6814  faclbnd 6833  faclbnd4lem4 6839  bccl2t 6860  climcl 6867  sumeq2 6874  fsum1s 6898  fsum1s2 6899  fsump1s 6902  fsumcllem 6903  fsum1ps 6907  fsumsplit 6909  fsumadd 6911  fsumcom 6917  fsumrev 6918  fsumshftm 6921  fsummulc1 6922  fsummulc2 6923  fsumdivc 6924  fsumdivcALT 6925  fsumconst 6927  fsumcmp 6929  fsumcmpndx2 6931  fsumabs 6932  clm3 6968  clm4le 6970  clm0 6972  clm0nns 6974  clmi2at 6980  climconst 6982  climunii 6986  2climnn 6990  2climnn0 6991  climshft 6992  iserzshft2 6995  climge0 7000  climaddc1 7005  climaddc2 7006  climmullem4 7010  climmullem5 7011  climmulc2 7016  climsubc2 7018  clim2serzt 7021  climcmplem 7024  climserzle 7034  climcau 7043  caucvglem2 7045  caucvglem6 7049  caucvg 7050  serzf0 7056  ser1f0 7057  ser1cmp2 7064  cvgcmp3cetlem1 7075  cvgcmp3cetlem2 7076  cvgcmp3cet 7077  isumclim2tf 7084  isumclt 7095  iserzgt0 7097  isumcmpi 7101  reccnv 7104  infcvglem3 7109  expcnv 7119  georeclim 7126  geoisumr 7129  cvgratlem2ALT 7134  cvgratlem3ALT 7135  cvgratlem1 7136  cvgratlem2 7137  cvgratlem3 7138  cvgratlem5 7140  fsum0diaglem2 7143  fsum0diag3 7146  fsum0diag4 7147  elcncf 7151  elcncf1d 7156  ivthlem9 7175  efaddlem23 7253  eftlext 7271  reeff1o 7319  xpnnen 7392  znnen 7396  unbenlem 7398  infpnlem1 7400  infxpidmlem7 7452  infxpidmlem10 7455  infxpidmlem11 7456  infmap2lem1 7472  alephexp1 7477  uniopnt 7491  tgclt 7517  tgss2t 7530  basgen2t 7532  subbas2 7538  subtop 7539  fctop 7543  cctop 7545  retopbas 7548  ntrval 7569  iincld 7572  clsval2 7578  0ntr 7594  elcls 7596  elcls3 7600  neii1 7610  neii2 7611  0nnei 7615  islp2 7636  clslp 7637  qdensere 7639  cnima 7654  cnclima 7658  cnsscnp 7659  cncnplem4 7664  cncnp 7665  metxplem3 7716  metxplem4 7721  metxp 7722  rnblssm 7739  blss 7741  ssbl 7743  opnuni 7756  opnin 7757  rnblopn 7762  metcnp 7774  metcn 7776  metcnpi3 7779  metcnpi4 7780  metcni2 7782  metcnss2 7786  metdnsconst 7788  cncfmet 7792  lmnn 7821  caun0 7828  lmsslem 7835  caussi 7837  metelcls 7848  metcnp4 7852  metcn4i 7854  xplmi 7855  xplm 7857  xpcn 7858  iscms2lem3 7873  iscms2lem4 7874  iscms2lem5 7875  lmcau 7878  cmsss 7879  bcthlem2 7882  bcthlem10 7890  bcthlem21 7901  bcthlem25 7905  bcthlem28 7908  bcthlem33 7913  bcth 7914  grpass 7929  grpidinvlem3 7932  grpidinvlem4 7933  grpid 7947  grpasscan1OLD 7956  grpasscan1 7960  grpnnncan2 7976  grplactf1o 7982  subgabl 8008  ghgrpilem2 8019  nvz 8173  nvcni 8203  nvlmle 8205  sspmval 8261  sspival 8266  sspimsval 8268  nmoub3i 8303  nmobndseqi 8307  nmlno0lem 8320  nmlnoubi 8323  nmblolbi 8326  isblo3i 8327  blocni 8331  ipasslem1 8356  ipasslem5 8360  ipdir 8368  ipass 8371  ipsubdir 8374  sspph 8381  ubthlem5 8399  ubthlem14 8408  ubthi 8410  htthlem7 8490  htthlem10 8493  htthlem12 8495  efifolem2 8551  shftefif1olem 8574  shftefif1olemOLD 8575  eff1i 8578  ghomgsg 8662  ghomf1olem 8663  findabrcl 8685  uninqs 8701  infi1 8706  ficli 8727  cdrci 8738  truni1 8743  esnnei 8750  hmeomap 8756  hmeocna 8757  hmeocnb 8758  cmphmp 8759  cnvhmpha 8763  cnvhmphb 8764  hmphre 8768  hmphtr 8769  hmeogrp 8776  qusp 8780  filint 8787  fipfil2 8789  fgsb 8794  efilcp 8795  infi 8798  fgsb2 8799  efilcp2 8800  cnfilca 8801  iintlem1 8826  trnij 8831  idosd 8871  rdmob 8875  cmpasso 8900  cmpassoh 8923  homgrf 8924  imonclem 8933  ismonc 8934  cmpmon 8935  icmpmon 8937  normpyct 9162  shelt 9231  shsubcltOLD 9241  chelt 9251  hlimcaui 9257  ocorth 9294  shorth 9298  ocnelt 9300  occl 9311  projlem13 9328  projlem15 9330  projlem26 9341  projlem27 9342  projlem28 9343  pjthlem13 9360  pjtheut 9365  pjpj0 9384  pjomlt 9398  shscl 9410  shsel1t 9414  chintcl 9424  shlej1t 9484  shmods 9491  shmod 9492  h1dn0 9604  spansn 9610  spansnmul 9617  spansnsst 9625  elspansn4t 9627  h1datom 9635  cm2jt 9694  osumlem4 9712  osumlem6 9714  spansncv 9728  5oalem6 9735  pjige0t 9767  pjsumt 9786  pjds 9788  pjds3 9789  homco1t 9858  homulasst 9859  eigret 9892  eigortht 9895  nmopub2tALT 9964  nmfnleub2t 9980  elnlfn2t 9983  kbpjt 10010  homco2t 10031  nmlnop0ALT 10049  nmopunt 10068  nmbdoplbt 10079  nmcopexlem1 10080  nmcopexlem6 10085  nmcoplbt 10089  nmcfnexlem1 10109  nmcfnexlem6 10114  nmcfnlbt 10118  nlelch 10123  branmfnt 10165  bra11 10168  cnvbravalt 10170  leopaddt 10191  leopmulit 10192  leopmul2it 10194  pjnmop 10200  pjnormss 10221  pjclem4 10251  pj3s 10259  hstel2t 10270  hst1ht 10278  stle 10291  stles 10292  stadd 10297  stadd3 10299  strlem3a 10303  hstrlem3a 10311  stcltrlem1 10327  spansncv2t 10344  mdslmd1lem3 10376  mdslmd1lem4 10377  csmdsym 10383  mdexch 10384  atss 10395  atsseq 10396  superpos 10403  chcv1t 10404  chjatom 10406  hatomict 10409  hatomistic 10411  cvbr3 10416  atcv1t 10429  atexcht 10430  atoml 10431  atoml2 10432  atcvatlem 10434  atcvat 10435  atcvat2 10436  irredlem3 10441  irredlem4 10442  atcvat3 10445  atcvat4 10446  mdsymlem3 10454  sumdmdi 10463  sumdmdlem 10466  sumdmdlem2 10467  dmdbr5at 10469  cdj1 10479  cdj3lem1 10480  cdj3lem2b 10483

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