Theorem imp 277

Description: Importation inference.

Hypothesis

Ref	Expression
imp.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
imp	|- ((ph /\ ps) -> ch)

Proof of Theorem imp

Step	Hyp	Ref	Expression
1		df-an 198	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2		imp.1	. . 3 |- (ph -> (ps -> ch))
3	2	impi 124	. 2 |- (-. (ph -> -. ps) -> ch)
4	1, 3	sylbi 174	1 |- ((ph /\ ps) -> ch)

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196

This theorem is referenced by:  pm3.35 278  imp31 280  imp32 281  imp4b 283  imp41 286  imp42 287  imp43 288  imp44 289  imp45 290  impac 304  adantl 305  adantr 306  adantll 309  adantlr 310  adantrl 311  adantrr 312  biimpa 324  biimpar 325  biimpac 326  biimparc 327  jaob 328  imdistani 340  sylan 343  sylan2 346  sylan9r 360  anabsi7 379  3imtr3g 425  ordi 452  jcad 455  elimant 505  msca 508  orcanai 515  mpan11 529  mpan12 530  mpan21 531  mpan22 532  mpan121 533  19.21ad 741  19.26 749  eqan 816  a4c1 844  eqvin.l1 851  hbsb4 905  ddelimf2 907  ddelimdf 909  sbcom 916  eqvin.l2 931  mopick 1054  moexex 1058  clneq 1168  clneq2 1169  rgen3 1265  r19.21bi 1266  r19.23ai 1283  r19.23advv 1288  r19.15 1292  gencl 1365  2gencl 1366  3gencl 1367  vtocl2gf 1385  vtocl2ga 1388  bisbcdv 1468  ssel2 1503  sstr 1511  sspsstr 1575  psssstr 1576  reupick 1578  neldif 1594  disjpss 1738  minel 1743  pssdifn0 1750  dedth2h 1787  dedth4h 1789  prel12 1875  prex 1892  pwssun 1917  ssuni 1937  reuuni1 1955  unipw 1960  iineq2 2007  ssiun 2018  poirr 2133  potr 2134  solin 2145  supmo 2156  supnub 2162  fri 2170  frirr 2176  fr2nr 2177  fr3nr 2178  tz7.2 2183  epfrc 2185  dfwe2 2187  wefrc 2195  wereu 2197  ordelss 2215  trssord 2216  nordeq 2218  ordelord 2221  tz7.7 2224  onfr 2237  tfi 2244  ordtr2 2257  oninton 2267  oneqmini 2272  limelon 2286  trsuc 2308  limsuclem 2360  limsuc 2361  unizlim 2364  limomss 2378  ordom 2382  nnsuc 2389  peano5 2394  findsg 2398  tfindsg 2402  tfindsg2 2403  brrelex 2446  optocl 2469  2optocl 2470  3optocl 2471  elreldm 2554  resieq 2581  imasn 2616  funssres 2698  fununi 2705  resfunexg 2717  fneu 2728  fnun 2730  fss 2759  fco 2760  opelf 2762  fun 2763  f1oun 2815  fv3 2839  funopfvg 2854  fvelima 2859  fvco 2865  fvco2 2866  fvopab3ig 2869  fvopab2 2878  fnressn 2897  fressnfv 2898  fconstfv 2903  funfvima2 2905  funfvima3 2906  f1fveq 2918  isorel 2932  isocnv 2934  isotr 2935  isotrALT 2936  isomin 2937  isoini 2938  isofrlem 2939  f1oweOLD 2944  tfrlem2 2950  tfrlem7 2955  tfrlem8 2956  tfrlem9 2957  tfrlem11 2959  tfr3 2964  rdglimt 2986  tz7.49 2997  abianfp 3000  ndmoprg 3057  ndmoprcl 3058  ndmord 3064  oevn0 3123  oacl 3138  omcl 3139  oecl 3140  oaordi 3148  oawordeu 3157  oawordexr 3158  oalimcl 3162  oaass 3163  omordi 3164  nnacl 3172  nnmcl 3173  nnacom 3175  nnmsucr 3182  nnmcom 3183  nnmordi 3188  nnmord 3189  nnmcan 3190  omsmolem 3195  omsmo 3196  ectocl 3238  ecoptocl 3239  2ecoptocl 3240  eceqopreq 3249  th3qlem1 3250  th3qlem2 3251  mapvalg 3263  en3d 3304  dom2d 3307  fundmen 3333  undom 3342  xpdom2 3345  pw2en 3348  sbthlem1 3349  ensdomtr 3372  domsdomtr 3374  enen1 3375  enen2 3376  domen1 3377  domen2 3378  sdomen1 3379  sdomen2 3380  mapenlem2 3385  mapen 3386  mapdom2 3389  mapunen 3397  limensuc 3402  nneneq 3408  php 3409  php3 3411  sucdomi 3419  finsucdom 3421  pssinf 3422  isfinite1 3425  infsdomnn 3426  pssnn 3428  ssfi 3430  unblem1 3431  unblem3 3433  isfinite2 3437  unfilem1 3438  fiint 3445  preleq 3454  suc11reg 3456  inf3lem1 3464  inf3lem5 3468  inf3lem6 3469  zfregs 3491  setind 3492  r1ord 3499  r1val1 3502  tz9.12lem3 3505  rankr1 3518  ssrankr1 3520  aceq3 3556  aceq5lem4 3561  aceq5 3563  aceq6b 3565  ac6lem 3575  ac6s 3577  kmlem2 3581  numthlem 3598  zornlem1 3603  zornlem4 3606  zornlem5 3607  zornlem6 3608  zornlem7 3609  fodom 3613  fodomb 3615  sucdom 3648  unxpdomlem 3649  cardlim 3657  ondomon 3662  carduni 3664  alephordi 3679  alephle 3689  cardaleph 3690  cardinfima 3696  cflim 3704  axrepndlem1 3738  axrepndlem2 3739  axrepnd 3740  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  mulclpi 3815  mulcanpi 3821  ltmpi 3825  indpi 3828  ltaddpq 3873  ltrpq 3879  elprpq 3889  prcdpq 3891  distrlem4pr 3924  psslinpr 3929  prlem934a 3931  prlem934 3933  ltaddpr 3934  ltexprlem3 3938  ltexprlem5 3940  ltaprlem 3944  prlem936 3949  suplem1pr 3955  mulcmpblnr 3977  recexsrlem 4006  mulgt0sr 4008  ssgt0sr 4011  suppsrlem 4015  suppsr2 4017  suppsr3 4018  supsrlem2 4020  suprelem 4053  axrecex 4079  axrrecex 4081  addcan 4120  negeu 4124  renegcl 4171  mulcan 4207  mulcant2 4209  receu 4215  divmult 4220  divclt 4223  divcan1t 4228  divcan2t 4229  divneq0bt 4230  recidt 4235  divrect 4238  divasst 4239  div23t 4240  divdistrt 4246  divcan3t 4251  divmuldivt 4263  divadddivt 4264  divdivdivt 4265  divdiv23t 4271  redivcl 4274  redivclt 4276  letrt 4291  addgegt0 4325  prodgt0 4388  divgt0 4390  divge0 4392  ledivt 4405  ltmuldiv2t 4407  ltdivmult 4408  nnaddclt 4436  nnmulclt 4437  lt1nnn 4442  nnleltp1t 4448  sup2 4510  suprub 4513  suprlub 4514  nnreclt 4522  crulem 4528  lt0nnn0 4549  elnnz 4572  elnnz1 4581  nn0subt 4587  zaddclt 4590  zmulclt 4596  zltp1let 4597  sqznn 4600  zneo 4601  uzind 4603  uzwo 4605  uzwo2 4606  nnwoOLD 4608  nn0ind 4612  zmax 4618  zbtwnre 4619  qaddclt 4642  qmulclt 4644  qrecclt 4646  qbtwnre 4650  om2uzlt 4654  seqrn 4673  expcllem 4682  le2sqet 4707  sqr0 4730  sqrlem12 4742  sqrclt 4767  sqrgt0t 4768  sqrge0t 4769  sqr00t 4770  sqsqrt 4776  sqr2irrlem3 4779  replimt 4798  xpnnen 4927  znnenlem 4929  znnen 4930  infxpidmlem7 4939  infxpidmlem10 4942  infxpidmlem11 4943  infmap2lem1 4951  infmap2 4953  alephexp1 4954  normpyct 5093  shelt 5118  shsubclt 5125  chelt 5135  hlimcaui 5141  chsscm 5147  ocorth 5172  shorth 5176  occllem6 5185  occl 5188  projlem13 5205  projlem15 5207  projlem26 5218  projlem27 5219  projlem28 5220  pjthut 5243  omlsi 5250  dfch2 5254  pjpj0 5259  shscl 5282  shsel1t 5286  chintcl 5296  shlej2t 5357  shmods 5363  shmod 5364  h1dn0 5457  spansn 5462  spansnmul 5469  elspansn2t 5472  spansneleq 5475  spansnsst 5476  elspansn4t 5478  h1datom 5483  osumlem4 5533  osumlem6 5535  spansncv 5542  5oalem6 5549  pjrn 5587  pjsumt 5590  pjss1co 5633  pjss2co 5634  pjnormss 5638  pjorthco 5639  pjscj 5640  pjclem4a 5652  pjclem4 5653  pj3lem1 5658  pj3s 5659  stle 5681  stles 5682  stadd 5687  stadd3 5689  strlem3a 5693  strlem4 5695  strlem5 5696  stcltrlem1 5709  cvnbtwnt 5718  spansncv2t 5725  mdi 5727  dmdi 5732  atss 5744  atsseq 5745  chcv1t 5751  hatomistic 5755  atcv1 5768  atexch 5769  atcvatlem 5770  atcvat 5771  atcvat2 5772  atcvat2t 5773  atcvat3 5774  atcvat4 5775  mdsymlem1 5776  mdsymlem3 5778  mdsymlem5 5780  sumdmdi 5785  sumdmdlem 5786  sumdmd 5787

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org