Theorem exp 291

Description: Exportation inference.

Hypothesis

Ref	Expression
exp.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
exp	|- (ph -> (ps -> ch))

Proof of Theorem exp

Step	Hyp	Ref	Expression
1		df-an 198	. . 3 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2		exp.1	. . 3 |- ((ph /\ ps) -> ch)
3	1, 2	sylbir 176	. 2 |- (-. (ph -> -. ps) -> ch)
4	3	expi 125	1 |- (ph -> (ps -> ch))

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

This theorem is referenced by:  exp31 293  exp32 294  exp4b 296  exp41 299  exp43 301  adantll 309  adantlr 310  adantrl 311  adantrr 312  anidms 332  sylan 343  sylan2 346  sylanc 361  pm2.61an1 364  pm2.61an2 365  anabss7 385  3imtr3g 425  ibib 448  jcad 455  elimant 505  msca 508  mpan 518  mpan2 519  mpdan 527  mpan11 529  mpan12 530  mpan21 531  mpan22 532  mpan121 533  biantrud 545  ecase3 559  19.21ad 741  a4c1 844  sbequ1 863  sbequi 876  hbsb4 905  ddelimf2 907  ddelimdf 909  sbcom 916  cbval2 974  cbvex2 975  sbcom2 992  sbal1 996  mo2 1026  moexex 1058  2moswap 1064  2eu2 1068  biralda 1213  birexda 1214  rgen2 1248  r19.20da 1255  rgen2a 1264  r19.21be 1269  nrexdv 1271  r19.22dva 1280  r19.23aivv 1287  r19.23advv 1288  bireudva 1317  2gencl 1366  3gencl 1367  vtocl2ga 1388  vtocl3ga 1389  ceqex 1410  sspss 1569  sspsstr 1575  psssstr 1576  reuss 1577  reupick 1578  reuhyp 1581  neldif 1594  pssdifn0 1750  prel12 1875  pwssun 1917  ssuni 1937  uniss2 1942  difex2 1951  reuuni4 1959  ssiun2 2019  iunpw 2040  opabsb 2114  sotrieq 2149  supmo 2156  supnub 2162  supsn 2168  efrirr 2180  dfwe2 2187  wefrc 2195  ordelord 2221  tz7.7 2224  onfr 2237  ordon 2238  tfi 2244  ssorduni 2249  ordtr2 2257  ordunidif 2260  onint 2261  onint0 2262  onintss 2266  oninton 2267  onnminsb 2271  oneqmini 2272  oneqmin 2273  onminex 2275  onmindif2 2313  onpwsuc 2315  ordsuc 2318  onsucmin 2323  ordsucelsuc 2324  ordtri2or2 2329  ordsucun 2333  unon 2338  limsuclem 2360  limsuc 2361  limsssuc 2362  unizlim 2364  dfom2 2374  limomss 2378  limom 2387  peano5 2394  nn0suc 2395  findsg 2398  tfinds 2401  tfindsg 2402  tfindsg2 2403  2optocl 2470  3optocl 2471  opres 2580  imasn 2616  dffun7 2688  imadif 2714  resfunexg 2717  fneu 2728  2elresin 2733  zfrep6 2744  fnopabg 2745  fun 2763  fcoi1 2765  fcoi2 2766  feu 2767  fcnvres 2768  f1oun 2815  tz6.12-1 2842  tz6.12c 2846  funbrfv 2852  fnopabfv 2858  fniunfv 2860  funfv 2862  fvco 2865  fvco2 2866  fvopabn 2873  cleqfv 2880  fvelrn 2883  fopab2 2891  ffnfv 2892  fsn 2895  fnressn 2897  fressnfv 2898  fconst2 2902  fconstfv 2903  funfvima 2904  funfvima2 2905  f1fv 2916  isocnv 2934  isotr 2935  isotrALT 2936  isomin 2937  isofrlem 2939  tfrlem1 2949  tfrlem2 2950  tfrlem5 2953  tfrlem8 2956  tfrlem9 2957  tfrlem10 2958  tfrlem11 2959  rdgsucopabn 2985  rdglim2 2987  tz7.48-2 2995  abianfplem 2999  abianfp 3000  eloprabg 3035  ndmoprcl 3058  oe0lem 3121  oevn0 3123  oalim 3135  omlim 3136  oacl 3138  omcl 3139  oecl 3140  oa0r 3141  om1r 3145  oe1m 3147  oaordi 3148  oawordri 3152  oawordeulem 3156  oawordexr 3158  oawordex 3159  oaordex 3160  oalimcl 3162  oaass 3163  omordi 3164  oen0 3165  nnacl 3172  nnacom 3175  nnmsucr 3182  nnmcom 3183  nnmordi 3188  nnmord 3189  erthi 3218  erdisj 3223  2ecoptocl 3240  brecop 3242  th3qlem1 3250  th3qlem2 3251  mapsn 3269  mapss 3270  breng 3280  brdomg 3281  en3d 3304  dom2d 3307  ensymg 3316  fundmen 3333  undom 3342  xpdom2 3345  pw2en 3348  sbthlem1 3349  sdomnsym 3364  sdomdomtr 3370  ensdomtr 3372  domsdomtr 3374  enen1 3375  enen2 3376  domen1 3377  domen2 3378  sdomen1 3379  mapenlem1 3384  mapenlem2 3385  mapen 3386  mapdom2 3389  mapxpen 3390  xpmapenlem3 3393  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  ssenen 3399  phplem5 3407  nneneq 3408  php 3409  php3 3411  onomeneq 3414  onfin 3415  nndomo 3416  pssinf 3422  ominf 3423  isfinite1 3425  infsdomnn 3426  pssnn 3428  ssnn 3429  ssfi 3430  unblem2 3432  unblem3 3433  isfinite2 3437  unfi 3441  suc11reg 3456  inf3lemd 3463  inf3lem1 3464  inf3lem5 3468  inf3lem6 3469  infensuc 3484  trcl 3489  zfregs 3491  r1tr 3498  r1ord 3499  r1val1 3502  rankr1 3518  ssrankr1 3520  r1val3 3523  r1pwcl 3530  rankonid 3538  rankr1id 3539  aceq5lem4 3561  aceq5 3563  aceq6b 3565  ac5b 3574  ac6lem 3575  ac6s 3577  kmlem10 3589  zornlem4 3606  zornlem6 3608  zornlem7 3609  fodomb 3615  imadomg 3616  hta 3619  cardnn 3631  carddomi 3641  sucdom 3648  sdomsdomcard 3654  cardlim 3657  ondomon 3662  ondomcard 3663  carduni 3664  cardiun 3665  cardmin 3666  alephon 3671  alephcard 3673  alephnbtwn 3674  alephordi 3679  alephord2i 3682  alephsucdom 3685  cardaleph 3690  cardalephex 3691  iscard3 3693  cardinfima 3696  cfub 3703  cflim 3704  axextnd 3737  axrepndlem1 3738  axrepndlem2 3739  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axpownd 3747  axregndlem1 3748  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  addclpi 3814  mulcanpi 3821  addnidpi 3822  ltexpi 3823  ltmpi 3825  nlt1pi 3827  indpi 3828  ordpipq 3850  ltexpq 3874  prcdpq 3891  genpnnp 3902  genpcd 3903  1pr 3911  distrlem4pr 3924  distrlem5pr 3925  1idpr 3927  prlem934 3933  ltexprlem2 3937  ltexprlem3 3938  ltexprlem4 3939  ltexprlem7 3942  ltexpri 3943  addcanpr 3946  prlem936b 3948  prlem936 3949  reclem2pr 3951  reclem3pr 3952  reclem4pr 3953  suplem1pr 3955  suplem2pr 3956  mulcmpblnr 3977  ltsrpr 3980  map2psrpr 4014  suppsr2 4017  suppsr3 4018  supsrlem2 4020  supsr 4025  axrecex 4079  axrnegex 4080  axrrecex 4081  addcan 4120  negeu 4124  addsubt 4151  mulcan 4207  receu 4215  divneq0bt 4230  div23t 4240  divmuldivt 4263  divadddivt 4264  divdiv23t 4271  leltnet 4287  letrt 4291  addgegt0 4325  ltmullem 4337  divge0 4392  ledivt 4405  ltmuldiv2t 4407  ltdivmult 4408  nn1suc 4435  nnaddclt 4436  nndiv 4453  sup2 4510  sup3 4511  nnunb 4520  crulem 4528  creur 4532  creui 4533  lt0nnn0 4549  nn0ge0t 4550  elnnz 4572  nn0subt 4587  zaddclt 4590  zrevaddclt 4592  elnn0nn 4593  zltp1let 4597  zneo 4601  peano2uz 4602  uzind 4603  uzwo 4605  nnwoOLD 4608  nn0ind 4612  btwnz 4613  uzwo3lem1 4614  qrecclt 4646  qrevaddclt 4648  qbtwnre 4650  om2uzlt 4654  om2uzran 4655  seqlem1 4662  seqrn 4673  expaddt 4698  le2sqet 4707  discrlem3 4715  nn0opthlem2 4723  sqrlem12 4742  sqr11 4761  sqr2irr 4782  replimt 4798  facclt 4874  znnen 4930  infxpidmlem1 4933  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem10 4942  infxpidmlem11 4943  infxpidmlem12 4944  infdif 4948  hiidge0t 5056  his6 5057  hial0 5058  normgt0t 5078  normpyct 5093  shsubclt 5125  hlimcaui 5141  chsscm 5147  chcmh 5148  ocsh 5164  occont 5168  ocorth 5172  occllem4 5183  occllem6 5185  occl 5188  projlem16 5208  projlem21 5213  projlem24 5216  projlem25 5217  projlem28 5220  projlem31 5223  pjthu 5241  pjthu2 5242  omlsi 5250  pjoml 5271  shsel1t 5286  shlej2t 5357  shmods 5363  h1de2b 5459  h1de2ctlem 5460  spansn 5462  spansncol 5473  spansneleq 5475  elspansn3t 5477  elspansn5t 5479  spansnss2t 5480  h1datom 5483  osumlem4 5533  osumlem5 5534  osumlem7 5536  spansncv 5542  pjjs 5585  pjsumt 5590  pjss1co 5633  pjss2co 5634  pjnormss 5638  pjorthco 5639  pjscj 5640  pjclem4 5653  pj3s 5659  stclt 5672  stge1 5679  stle0 5680  stle 5681  stadd 5687  stadd3 5689  strlem1 5691  strlem3a 5693  str 5698  stcltrlem1 5709  stcltrth 5711  cvcon3t 5716  cvnbtwnt 5718  spansncv2t 5725  mdbr3 5729  mdbr4 5730  dmdbr 5731  atsseq 5745  h1dat 5747  chcv1t 5751  shatomic 5753  hatomistic 5755  atcv0eq 5767  atcv1 5768  atexch 5769  atcvatlem 5770  atcvat 5771  atcvat2 5772  atcvat3 5774  atcvat4 5775  mdsymlem4 5779  mdsymlem6 5781  sumdmdi 5785  sumdmdlem 5786

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