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 681  biantrud 726  dedlemb 763  cbval2 1316  cbvex2 1317  mo2 1400  2moswap 1444  2mos 1448  2eu2 1450  r19.21be 1728  rcla4dv 1878  rcla4edv 1879  sbcel12g 2011  sbceqdig 2012  difsn 2464  ssuni 2522  uniss2 2529  elssabg 2726  elpw2g 2727  elpwuni 2761  difex2 2877  reuuni4 2887  onfr 2986  ordpwsuc 3066  ordsucun 3082  limuni3 3123  relop 3275  opres 3375  xp11 3476  funopg 3547  fneu 3592  fun 3641  tz6.12-1 3736  tz6.12c 3740  fnressn 3837  fressnfv 3838  fconst2g 3845  eloprabg 4007  ndmoprcl 4044  oacl 4170  oawordri 4184  oalimcl 4194  oaass 4195  omwordri 4203  oeordi 4214  nnacl 4229  nnacom 4233  nnmsucr 4240  th3qlem2 4315  elmapg 4333  mapsn 4345  mapss 4346  f1domg 4396  f1dom2g 4397  ssdom2g 4409  enen2 4478  domen2 4480  pwuninel 4486  mapunen 4502  php 4513  php3 4515  php3OLD 4516  isfinite1OLD 4531  infsdomnn 4532  ssnnfi 4535  ssnnfiOLD 4536  unfi 4551  unfiOLD 4552  inf3lemd 4612  inf3lem5 4617  rankr1 4674  rankxplim3 4714  aceq5 4740  ac6lem 4754  ac6s 4756  imadomg 4806  unidom 4808  cardnn 4824  ondomon 4856  ondomcard 4857  alephordi 4874  iscard3 4888  carduniima 4890  axregndlem1 4954  axregnd 4956  addclpi 5020  addnidpi 5028  prlem936b 5154  reclem3pr 5158  mulcmpblnr 5183  map2psrpr 5220  ltmullem 5640  nn1suc 5939  nnaddclt 5940  nndivt 5959  sup3 6052  zrevaddclt 6170  zneo 6200  uzwo4OLD 6210  qrevaddclt 6275  qbtwnre 6278  om2uzlt 6298  ser1recl 6331  ndmioo 6370  icoshft 6408  icounlem 6412  snunioolem 6414  uzwo 6455  uzwoOLD 6456  seqzeq 6555  seqzrn 6557  expaddt 6596  expmult 6597  expord2t 6604  expmwordit 6606  creui 6743  mulretOLD 6777  ser1absdiflem 6929  facclt 6940  facdivt 6942  faclbnd 6945  faclbnd4lem4 6951  faclbnd6 6954  fsumdivc 7035  fsumdivcALT 7036  bcxmas 7076  clm3 7079  iserzshft2 7107  climaddlem3 7116  climmullem8 7127  clim2serzt 7134  iserzext 7135  iserzmulc1 7136  iserzcmp 7142  climabslem 7148  serzf0 7169  ser1f0 7170  isumreclt 7210  iserzgt0 7211  isummulc1ALT 7213  isumcmpi 7215  elcncf 7265  rescncf 7272  cncffvrn 7273  abscncflem 7274  mulc1cncf 7279  divccncf 7280  ivthlem7 7287  efexpt 7372  effsumle 7397  efcn 7423  sin01bndlem2 7468  cos01bndlem2 7470  sin01gt0 7476  sin02gt0 7478  infxpidmlem8 7559  infxpidmlem12 7563  infdif 7568  fctopOLD 7650  isnei 7718  cnsscnp 7772  mettri 7817  opnuni 7868  metcnp 7887  metcnss 7898  metcnss2 7899  cmsss 7997  bcthlem7 8005  bcthlem26 8024  bcthlem29 8027  grplactf1o 8098  ring2 8149  sqcn 8335  nmobndi 8438  ubthlem6 8534  efif1lem5 8734  occllem6 9178  osumlem4 9581  stle0 10166  strlem3a 10179  hstrlem3a 10187  hstrb 10193  spansncv2t 10220  h1dat 10276  elghomlem2 10383  ghomf1olem 10396  nndivsub 10421  rcla4devOLD 10431  uninqs 10441  elo 10444  infi1 10447  infi1OLD 10448  fiiu2 10488  fiiu2OLD 10489  truni1 10499  hmeogrp 10538  homcard 10539  filintf 10569  fgsb 10570  fgsbOLD 10571  fisub 10576  fisubOLD 10577  fgsb2 10580  rcfpfillem4 10591  rcfpfillem4OLD 10592  ltsubpostb 10627  ltaddpos2tb 10628  trran 10636  trnij 10637  imonclem 10741

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