Theorem expcom 372

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 371	. 2 |- (ph -> (ps -> ch))
3	2	com12 11	1 |- (ps -> (ph -> ch))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  bibif 685  biantrud 731  dedlemb 768  cbval2 1354  cbvex2 1355  mo2 1439  2moswap 1484  2mos 1488  2eu2 1490  r19.21be 1774  rcla4dv 1924  rcla4edv 1925  sbc2ie 2036  sbcel12g 2062  sbceqdig 2063  difsn 2528  ssuni 2589  uniss2 2596  elpwuni 2689  elssabg 2800  elpw2g 2801  onfr 3014  difex2 3101  reuuni4 3110  ordpwsuc 3172  ordsucun 3180  limuni3 3206  relop 3365  opres 3462  funopg 3652  fneu 3698  fun 3748  tz6.12-1 3847  tz6.12c 3851  fnressn 3951  fressnfv 3952  fconst2g 3959  eloprabg 4067  ndmoprcl 4105  fo1stres 4156  oacl 4306  oawordri 4320  oalimcl 4330  oaass 4331  omwordri 4339  oeordi 4350  oeoelem 4361  nnacl 4369  nnacom 4373  nnmsucr 4380  th3qlem2 4456  elmapg 4474  mapsn 4486  mapss 4487  f1domg 4537  f1dom2g 4538  ssdom2g 4550  ac6sfilem3 4590  enen2 4623  domen2 4625  pwuninel 4631  mapunen 4649  php 4660  php3 4662  isfinite1 4677  infsdomnn 4678  ssnnfi 4682  unfi 4697  inf3lemd 4757  inf3lem5 4762  rankr1 4820  rankxplim3 4860  aceq5 4886  ac6lem 4900  ac6s 4902  imadomg 4952  unidom 4954  cardnn 4970  ondomon 5006  ondomcard 5007  alephordi 5024  iscard3 5038  carduniima 5040  nnacda 5090  axregndlem1 5108  axregnd 5110  addclpi 5174  addnidpi 5182  prlem936b 5308  reclem3pr 5312  mulcmpblnr 5337  map2psrpr 5374  ltmullem 5794  nn1suc 6084  nnaddcl 6085  nndiv 6105  sup3 6220  zrevaddcl 6338  zdiv 6356  zneo 6371  uzwo4OLD 6381  qrevaddcl 6414  irradd 6416  irrmul 6417  qbtwnre 6418  ndmioo 6496  icoshft 6535  icounlem 6539  snunioolem 6541  uzwo 6582  uzwoOLD 6583  fzen 6622  om2uzlti 6661  ser1recli 6696  seqzeq 6750  seqzrn 6752  expadd 6791  expmul 6792  expord2 6801  expmwordi 6803  creui 6944  ser1absdiflem 7132  faccl 7143  facdiv 7145  faclbnd 7148  faclbnd4lem4 7154  faclbnd6 7157  fsumdivc 7238  fsumdivcALT 7239  bcxmas 7279  clm3i 7282  iserzshft2i 7310  climaddlem3 7319  climmullem8 7330  clim2serz 7337  iserzex 7338  iserzmulc1 7339  iserzcmp 7345  climabslem 7351  serzf0i 7372  isumrecl 7414  iserzgt0 7415  isummulc1iALT 7417  isumcmpii 7419  elcncf 7470  rescncf 7477  cncffvrn 7478  abscncflem 7479  mulc1cncf 7484  divccncf 7485  ivthlem7 7492  efexp 7577  effsumlei 7605  efcn 7631  sin01bndlem2 7677  cos01bndlem2 7679  sin01gt0 7685  infxpidmlem8 7771  infxpidmlem12 7775  infdif 7780  isnei 7928  cnsscnp 7982  mettri 8027  opnuni 8078  metequiv 8091  metcnp 8098  metcnss 8109  metcnss2 8110  cmsss 8208  bcthlem7 8216  bcthlem26 8235  bcthlem29 8238  grplactf1o 8339  ring2 8391  vacnlem3 8584  vacnlem6 8587  sqcn 8589  nmobndi 8692  ubthlem6 8792  efif1lem5 9006  occllem6 9454  osumlem4 9859  stle0i 10447  strlem3a 10460  hstrlem3a 10468  hstrbi 10474  spansncv2 10501  h1da 10557  elghomlem2 10668  ghomf1olem 10681  nndivsub 10706  uninqs 10730  elo 10733  infi1 10735  imgfldref2 10768  twpar2 10773  f1ofi 10778  fldsqcp2 10780  cpref 10782  islfin 10799  sfseqeq 10824  jidd 10840  midd 10841  fiiu2 10852  inposet 10868  pospos 10882  toplat 10884  exidu1 10902  rnplrnml0 10946  rnplrnml3 10950  unmnd 10951  truni1 10999  hmeogrp 11044  homcard 11045  subtopsin2 11067  filintf 11081  fgsb 11082  fisub 11085  fgsb2 11086  rcfpfillem4 11092  limfillem2 11102  stfincomp 11122  usinuniop 11128  clindistop 11131  altretop 11144  ltsubpostb 11150  ltaddpos2tb 11151  trran 11159  trnij 11160  imonclem 11268  isepic 11279  dmsdtriord 11408  finminlem 11418  fictblem 11422  omsubsdomlem2 11441  omsubsdom 11442  omsubel 11444  elomsubsd 11446  opncldf1 11454  cnsubsp2 11484  compsub 11488  hscptsscld 11491  compfipin0 11493  alexsublem3 11498  alexsub 11500  topbasfne 11560  fnessref 11564  lfinpfin 11574  comppfsc 11578  neibastop2lem1 11580  fbasfip 11627  fgfil 11638  hausfillim 11685  cnpfillim 11686  fclusbas 11722  gapm 11784  ficard 11834  inficl 11849  sdclem1 11875  sdclem2 11876  sdc 11877  seqpo 11878  metf1o 11907  metsstop 11909  iccss2 11921  cnss 11953  ishomeo2 11957  lmtlm 11969  sstotbnd 11992  isismty 12004  heiborlem15 12025  heiborlem23 12033  heiborlem41 12051  rrncms 12075  rrntotbnd 12078  phtpcer 12104

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 145  df-an 223

Copyright terms: Public domain