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 4393  en3d 4400  dom2d 4403  fundmen 4427  undom 4436  xpdom2 4440  pw2en 4444  sbthlem1 4445  ensdomtr 4469  domsdomtr 4474  enen1 4475  enen2 4476  domen1 4477  domen2 4478  sdomen1 4479  sdomen2 4480  fodomr 4481  mapenlem2 4488  mapen 4489  mapdom2 4492  mapunen 4500  nneneq 4510  php 4511  php3 4513  finsucdom 4524  pssinf 4525  isfinite1 4528  infsdomnn 4529  pssnn 4531  ssfi 4533  domfi 4534  unblem3 4537  isfinite2 4541  unfilem1 4543  unifi 4550  fiint 4552  abfii4 4556  fodomfi 4558  fodomfib 4559  pm54.43 4564  supmo 4568  supnub 4574  suppr 4582  suc11reg 4597  inf3lem1 4605  inf3lem5 4609  inf3lem6 4610  unbnnt 4631  zfregs 4639  setind 4640  r1ord 4647  r1val1 4650  tz9.12lem3 4653  rankr1 4666  ssrankr1 4668  rankxplim3 4706  rankxpsuc 4707  aceq3 4725  aceq5lem4 4730  aceq5 4732  aceq6b 4734  ac6s 4748  numthlem 4775  zorn2lem1 4780  zorn2lem4 4783  zorn2lem5 4784  zorn2lem6 4785  zorn2lem7 4786  fodomb 4792  unidom 4800  uniimadom 4802  sucdom 4834  unxpdomlem 4835  cardlim 4843  ondomon 4848  carduni 4850  alephordi 4866  alephle 4876  cardaleph 4877  cardinfima 4883  alephval2 4894  alephval3 4895  cflim 4901  axrepndlem1 4936  axrepndlem2 4937  axrepnd 4938  axpowndlem4 4944  axinfndlem1 4949  axacndlem4 4954  axacndlem5 4955  axacnd 4956  mulclpi 5013  mulcanpi 5019  ltmpi 5023  indpi 5026  ltaddpq 5071  ltrpq 5077  elprpq 5087  prcdpq 5089  distrlem4pr 5122  psslinpr 5127  prlem934a 5129  prlem934 5131  ltaddpr 5132  ltexprlem3 5136  ltexprlem5 5138  ltaprlem 5142  prlem936 5147  suplem1pr 5153  mulcmpblnr 5175  recexsrlem 5204  mulgt0sr 5206  ssgt0sr 5209  suppsrlem 5213  suppsr2 5215  suppsr3 5216  suprelem 5251  axrrecex 5276  cnegextlem1 5337  cnegextlem2 5338  addcan 5343  renegcl 5408  letrt 5517  xrletrt 5556  xrret 5561  xrre2t 5562  addgegt0 5592  msqgt0t 5607  gt0ne0t 5610  addgt0t 5638  addgegt0t 5639  addge0t 5641  mulge0t 5670  recext 5675  mulcan 5677  mulcanOLD 5678  mulcan2tOLD 5681  divmult 5695  recne0t 5720  recidt 5723  div23t 5730  div13t 5731  div12t 5732  divdirtOLD 5739  divmuldivt 5768  divadddivt 5772  divdivdivt 5773  redivcl 5786  prodgt0 5807  prodge0 5808  prodgt0t 5814  prodgt02t 5815  prodge0t 5816  prodge02t 5817  ltmul1t 5818  ltmul12it 5829  lemul12itOLD 5831  mulgt1t 5833  ltdiv1tOLD 5838  lediv1tOLD 5840  ltmuldivtOLD 5852  ltmuldiv2tOLD 5854  ltdivmultOLD 5856  ledivmultOLD 5857  lemuldiv2tOLD 5865  ltrect 5872  lerect 5873  lt2msqt 5874  lediv12it 5884  le2msqt 5891  ledivp1t 5893  ledivp1 5894  ltdivp1 5895  lt1nnn 5935  nnleltp1t 5942  nndivtrt 5948  lble 6035  sup2 6039  suprub 6044  suprlub 6045  suprnub 6046  suprleub 6047  infmrcl 6057  xrsupsslem 6064  xrinfmsslem 6065  xrub 6068  supxr 6069  supxrre 6071  supxrun 6073  supxrunb1 6077  supxrunb2 6078  supxrbnd 6079  supxrub 6086  supxrleub 6087  dfn2 6100  lt0nnn0 6104  nnnn0addclt 6113  elnnz 6133  elnnz1 6143  nn0subt 6149  zaddclt 6153  zmulclt 6168  zltp1let 6169  btwnnzt 6180  zneo 6188  uzind2 6194  uzindOLD 6196  uzwo4OLD 6198  nn0ind-raph 6202  zbtwnre 6209  qaddclt 6255  qmulclt 6257  qrecclt 6259  qbtwnre 6264  qsqueeze 6266  rpmulclt 6277  monoord 6280  seq1rn2 6307  ser1add2 6324  ser1add 6325  iooss1 6359  iooss2 6360  elioo4g 6371  iccsupr 6384  icoshft 6394  icounlem 6398  icoun 6399  ioojoint 6402  eluzt 6412  uz11t 6418  eluzp1m1t 6419  uzwo 6441  uzwoOLD 6442  elfzel2g 6466  elfz2nn0t 6481  elfz3nn0t 6483  fznn0subt 6484  fsequb 6509  fsequb2 6510  fseqsupcl 6511  fseqsupub 6512  seqzfveq 6540  seqzrn2 6542  expp1t 6560  expordit 6586  expcant 6587  expordt 6588  expword2it 6591  exple1t 6593  expubndt 6594  sq11t 6615  sq01t 6637  expnbndt 6640  expnlbndt 6641  sqr0 6658  sqrlem12 6670  sqrclt 6696  sqrgt0t 6697  sqrge0t 6698  sqrlet 6699  sqr00t 6700  sqrsqt 6708  sqsqrt 6709  crulem 6722  replimt 6747  absrpclt 6840  absidt 6847  absnidt 6848  leabst 6849  abssubne0t 6867  absmaxt 6882  seq1bnd 6895  cau2 6898  cau5i 6902  cvg3 6908  caubnd 6911  faclbnd 6930  faclbnd4lem4 6936  bccl2t 6956  climcl 6963  sumeq2 6970  fsum1s 6994  fsum1s2 6995  fsump1s 6998  fsumcllem 6999  fsum1ps 7003  fsumsplit 7005  fsumadd 7007  fsumcom 7013  fsumrev 7014  fsumshftm 7017  fsummulc1 7018  fsummulc2 7019  fsumdivc 7020  fsumdivcALT 7021  fsumconst 7023  fsumcmp 7025  fsumcmpndx2 7027  fsumabs 7028  clm3 7064  clm4le 7066  clm0 7068  clm0nns 7070  clmi2at 7076  climconst 7079  climunii 7083  2climnn 7087  2climnn0 7088  climshft 7089  iserzshft2 7092  climge0 7097  climabs0 7098  climaddc1 7103  climaddc2 7104  climmullem4 7108  climmullem5 7109  climmulc2 7114  climsubc2 7116  clim2serzt 7119  climcmplem 7122  climserzle 7132  climcau 7141  caucvglem2 7143  caucvglem6 7147  caucvg 7148  serzf0 7154  ser1f0 7155  ser1cmp2 7162  cvgcmp3cetlem1 7173  cvgcmp3cetlem2 7174  cvgcmp3cet 7175  isumclim2tf 7183  isumclt 7194  iserzgt0 7196  isumcmpi 7200  reccnv 7203  infcvglem3 7208  expcnv 7218  georeclim 7225  geoisumr 7228  cvgratlem2ALT 7233  cvgratlem3ALT 7234  cvgratlem1 7235  cvgratlem2 7236  cvgratlem3 7237  cvgratlem5 7239  fsum0diaglem2 7242  fsum0diag3 7245  fsum0diag4 7246  elcncf 7250  elcncf1d 7255  ivthlem9 7274  efaddlem23 7345  eftlext 7363  reeff1o 7411  xpnnen 7484  znnen 7487  unbenlem 7489  infpnlem1 7491  infxpidmlem7 7543  infxpidmlem10 7546  infxpidmlem11 7547  infmap2lem1 7564  alephexp1 7569  uniopnt 7583  tgclt 7609  tgss2t 7622  basgen2t 7624  subbas2 7630  subtop 7631  fctop 7635  cctop 7637  retopbas 7640  ntrval 7661  iincld 7664  clsval2 7670  0ntr 7687  elcls 7689  elcls3 7696  neii1 7706  neii2 7707  0nnei 7711  islp2 7732  clslp 7733  qdensere 7736  cnima 7752  cnclima 7756  cnsscnp 7757  cncnplem4 7762  cncnp 7763  metxplem3 7813  metxplem4 7818  metxp 7819  rnblssm 7836  blss 7838  ssbl 7840  opnuni 7853  opnin 7854  rnblopn 7859  metcnp 7872  metcn 7874  metcnpi3 7877  metcnpi4 7878  metcni2 7880  metcnss2 7884  metdnsconst 7886  cncfmet 7890  lmnn 7920  caun0 7930  lmsslem 7937  caussi 7939  metelcls 7950  metcnp4 7955  metcn4i 7957  xplmi 7958  xplm 7960  xpcn 7961  iscms2lem3 7976  iscms2lem4 7977  iscms2lem5 7978  lmcau 7981  cmsss 7982  bcthlem2 7985  bcthlem10 7993  bcthlem21 8004  bcthlem25 8008  bcthlem28 8011  bcthlem33 8016  bcth 8017  grpass 8032  grpidinvlem3 8035  grpidinvlem4 8036  grpid 8050  grpasscan1 8062  grpnnncan2 8078  grplactf1o 8083  subgabl 8108  ghgrpilem2 8119  nvz 8282  nvcni 8314  nvcni2 8315  nvcni3 8316  nvlmle 8318  sspmval 8377  sspival 8382  sspimsval 8384  nmoub3i 8421  nmobndseqi 8425  nmlno0lem 8438  nmlnoubi 8441  lnon0 8443  nmblolbi 8445  isblo3i 8446  blocni 8450  ipasslem1 8475  ipasslem5 8479  ipdir 8487  ipass 8490  ipsubdir 8493  sspph 8500  ubthlem5 8518  ubthlem14 8527  ubthi 8529  htthlem7 8611  htthlem10 8614  htthlem12 8616  psref 8634  spwmo 8641  spwpr4OLD 8648  spwpr4aOLD 8649  efifolem2 8708  shftefif1olem 8726  eff1i 8729  normpyct 8998  shelt 9065  shsubcltOLD 9075  chelt 9085  hlimcaui 9091  ocorth 9149  shorth 9153  ocnelt 9155  occl 9166  projlem13 9183  projlem15 9185  projlem26 9196  projlem27 9197  projlem28 9198  pjthlem13 9216  pjtheut 9221  pjpj0 9240  pjomlt 9254  shscl 9266  shsel1t 9270  chintcl 9280  shlej1t 9340  shmods 9347  shmod 9348  h1dn0 9460  spansn 9465  spansnmul 9472  spansnsst 9479  elspansn4t 9481  h1datom 9489  cm2jt 9548  osumlem4 9566  osumlem6 9568  spansncv 9582  5oalem6 9589  pjige0t 9621  pjsumt 9640  pjds 9642  pjds3 9643  homco1t 9712  homulasst 9713  eigret 9746  eigortht 9749  nmopub2tALT 9818  nmfnleub2t 9835  elnlfn2t 9838  kbpjt 9865  homco2t 9886  nmlnop0ALT 9905  nmopunt 9924  nmbdoplbt 9935  nmcopexlem1 9936  nmcopexlem6 9941  nmcoplbt 9945  nmcfnexlem1 9965  nmcfnexlem6 9970  nmcfnlbt 9974  nlelch 9979  branmfnt 10023  bra11 10026  cnvbravalt 10028  leopaddt 10050  leopmulit 10051  leopmul2it 10053  leoptrt 10055  pjnmop 10060  pjnormss 10081  pjclem4 10112  pj3s 10120  hstel2t 10131  hst1ht 10139  stle 10152  stles 10153  stadd 10158  stadd3 10160  strlem3a 10164  hstrlem3a 10172  stcltrlem1 10188  spansncv2t 10205  mdslmd1lem3 10239  mdslmd1lem4 10240  csmdsym 10246  mdexch 10247  atss 10258  atsseq 10259  superpos 10266  chcv1t 10267  chjatom 10269  hatomict 10272  hatomistic 10274  cvbr3 10279  atcv1t 10292  atexcht 10293  atoml 10294  atoml2 10295  atcvatlem 10297  atcvat 10298  atcvat2 10299  irredlem3 10304  irredlem4 10305  atcvat3 10308  atcvat4 10309  mdsymlem3 10317  sumdmdi 10327  sumdmdlem 10330  sumdmdlem2 10331  dmdbr5at 10334  cdj1 10345  cdj3lem1 10346  cdj3lem2b 10349  ghomgsg 10380  ghomf1olem 10381  findabrcl 10403  ee7.2a 10410  uninqs 10425  infi1 10430  ficli 10451  f2imacnv 10453  oooeqim2 10454  cdrci 10466  truni1 10471  esnnei 10480  hmeomap 10490  hmeocna 10491  hmeocnb 10492  cmphmp 10493  cnvhmpha 10497  cnvhmphb 10498  hmphre 10502  hmphtr 10503  hmeogrp 10510  homcard 10511  qusp 10515  filint 10522  fipfil2 10524  fgsb 10529  efilcp 10530  infi 10534  fgsb2 10535  efilcp2 10536  cnfilca 10537  rcfpfillem4 10541  limfillem2 10551  iintlem1 10575  trnij 10580  idosd 10620  rdmob 10624  cmpasso 10649  cmpassoh 10672  homgrf 10673  imonclem 10682  ismonc 10683  cmpmon 10684  icmpmon 10686  idmon 10687

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