Theorem expcom 374

Description: Exportation inference with commuted antecedents.

Hypothesis

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

Assertion

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

Proof of Theorem expcom

Step	Hyp	Ref	Expression
1		exp.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	ex 373	. 2 |- (ph -> (ps -> ch))
3	2	com12 11	1 |- (ps -> (ph -> ch))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  bibif 679  biantrud 724  dedlemb 761  cbval2 1311  cbvex2 1312  mo2 1393  2moswap 1437  2mos 1441  2eu2 1443  r19.21be 1720  rcla4dv 1869  rcla4edv 1870  sbcel12g 2001  sbceqdig 2002  difsn 2455  ssuni 2512  uniss2 2519  elssabg 2716  elpw2g 2717  elpwuni 2751  difex2 2867  reuuni4 2877  onfr 2976  ordpwsuc 3056  ordsucun 3072  limuni3 3113  relop 3265  opres 3359  xp11 3463  funopg 3533  fneu 3578  fun 3626  tz6.12-1 3721  tz6.12c 3725  fnressn 3822  fressnfv 3823  fconst2g 3830  eloprabg 3992  ndmoprcl 4030  oacl 4154  oawordri 4168  oalimcl 4178  oaass 4179  omwordri 4187  oeordi 4198  nnacl 4213  nnacom 4217  nnmsucr 4224  th3qlem2 4299  elmapg 4317  mapsn 4329  mapss 4330  f1domg 4377  f1dom2g 4378  ssdom2g 4390  enen2 4458  domen2 4460  pwuninelg 4467  mapunen 4482  php 4493  php3 4495  isfinite1 4510  infsdomnn 4511  ssnn 4514  unfilem3 4526  unfi 4528  inf3lemd 4584  inf3lem5 4589  rankr1 4646  rankxplim3 4686  aceq5 4712  ac6lem 4726  ac6s 4728  imadomg 4778  unidom 4780  cardnn 4796  ondomon 4828  ondomcard 4829  alephordi 4846  iscard3 4860  carduniima 4862  axregndlem1 4926  axregnd 4928  addclpi 4992  addnidpi 5000  prlem936b 5126  reclem3pr 5130  mulcmpblnr 5155  map2psrpr 5192  ltmullem 5614  nn1suc 5887  nnaddclt 5888  nndivt 5906  sup3 5999  zrevaddclt 6117  zneo 6147  zneoOLD 6148  uzwo4OLD 6158  qrevaddclt 6213  qbtwnre 6216  om2uzlt 6235  ser1recl 6268  ndmioo 6307  icoshft 6341  icounlem 6345  snunioolem 6347  uzwo 6387  uzwoOLD 6388  seqzeq 6487  seqzrn 6489  expaddt 6527  expmult 6528  expord2t 6535  expmwordit 6537  creui 6674  ser1absdiflem 6866  facclt 6877  facdivt 6879  faclbnd 6882  faclbnd4lem4 6888  faclbnd6 6891  fsumdivc 6973  fsumdivcALT 6974  bcxmas 7014  clm3 7017  iserzshft2 7044  climaddlem3 7052  climmullem8 7063  clim2serzt 7070  iserzext 7071  iserzmulc1 7072  iserzcmp 7078  climabslem 7084  serzf0 7105  ser1f0 7106  isumreclt 7145  iserzgt0 7146  isummulc1ALT 7148  isumcmpi 7150  elcncf 7200  rescncf 7207  cncffvrn 7208  abscncflem 7209  mulc1cncf 7214  divccncf 7215  ivthlem7 7222  ivthlem7OLD 7231  efexpt 7314  effsumle 7338  efcn 7363  sin01bndlem2 7410  cos01bndlem2 7412  sin01gt0 7418  sin02gt0 7420  infxpidmlem8 7502  infxpidmlem12 7506  infdif 7511  fctop 7592  isnei 7659  cnsscnp 7711  mettri 7756  opnuni 7808  metcnp 7826  metcnss 7837  metcnss2 7838  cmsss 7931  bcthlem7 7939  bcthlem26 7958  bcthlem29 7961  grplactf1o 8034  ring2 8086  sqcn 8270  nmobndi 8370  ubthlem6 8465  efif1lem5 8649  occllem6 9094  osumlem4 9498  stle0 10076  strlem3a 10089  hstrlem3a 10097  hstrb 10103  spansncv2t 10130  h1dat 10184  elghomlem2 10288  ghomf1olem 10301  rcla4devOLD 10331  uninqs 10342  elo 10345  infi1 10347  fiiu2 10377  truni1 10386  hmeogrp 10425  homcard 10426  filintf 10443  fgsb 10444  fisub 10447  fgsb2 10449  ltsubpostb 10471  ltaddpos2tb 10472  trran 10480  trnij 10481  imonclem 10583

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