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 680  biantrud 725  dedlemb 762  cbval2 1315  cbvex2 1316  mo2 1399  2moswap 1443  2mos 1447  2eu2 1449  r19.21be 1726  rcla4dv 1875  rcla4edv 1876  sbcel12g 2008  sbceqdig 2009  difsn 2461  ssuni 2518  uniss2 2525  elssabg 2722  elpw2g 2723  elpwuni 2757  difex2 2873  reuuni4 2883  onfr 2982  ordpwsuc 3062  ordsucun 3078  limuni3 3119  relop 3271  opres 3371  xp11 3472  funopg 3543  fneu 3588  fun 3636  tz6.12-1 3731  tz6.12c 3735  fnressn 3832  fressnfv 3833  fconst2g 3840  eloprabg 4002  ndmoprcl 4039  oacl 4163  oawordri 4177  oalimcl 4187  oaass 4188  omwordri 4196  oeordi 4207  nnacl 4222  nnacom 4226  nnmsucr 4233  th3qlem2 4308  elmapg 4326  mapsn 4338  mapss 4339  f1domg 4386  f1dom2g 4387  ssdom2g 4399  enen2 4467  domen2 4469  pwuninel 4475  mapunen 4491  php 4502  php3 4504  isfinite1 4519  infsdomnn 4520  ssnn 4523  unfi 4537  inf3lemd 4595  inf3lem5 4600  rankr1 4657  rankxplim3 4697  aceq5 4723  ac6lem 4737  ac6s 4739  imadomg 4789  unidom 4791  cardnn 4807  ondomon 4839  ondomcard 4840  alephordi 4857  iscard3 4871  carduniima 4873  axregndlem1 4937  axregnd 4939  addclpi 5003  addnidpi 5011  prlem936b 5137  reclem3pr 5141  mulcmpblnr 5166  map2psrpr 5203  ltmullem 5624  nn1suc 5897  nnaddclt 5898  nndivt 5916  sup3 6009  zrevaddclt 6127  zneo 6157  zneoOLD 6158  uzwo4OLD 6168  qrevaddclt 6225  qbtwnre 6228  om2uzlt 6248  ser1recl 6281  ndmioo 6320  icoshft 6354  icounlem 6358  snunioolem 6360  uzwo 6400  uzwoOLD 6401  seqzeq 6500  seqzrn 6502  expaddt 6541  expmult 6542  expord2t 6549  expmwordit 6551  creui 6689  ser1absdiflem 6881  facclt 6892  facdivt 6894  faclbnd 6897  faclbnd4lem4 6903  faclbnd6 6906  fsumdivc 6988  fsumdivcALT 6989  bcxmas 7029  clm3 7032  iserzshft2 7060  climaddlem3 7069  climmullem8 7080  clim2serzt 7087  iserzext 7088  iserzmulc1 7089  iserzcmp 7095  climabslem 7101  serzf0 7122  ser1f0 7123  isumreclt 7162  iserzgt0 7163  isummulc1ALT 7165  isumcmpi 7167  elcncf 7217  rescncf 7224  cncffvrn 7225  abscncflem 7226  mulc1cncf 7231  divccncf 7232  ivthlem7 7239  ivthlem7OLD 7248  efexpt 7331  effsumle 7355  efcn 7380  sin01bndlem2 7427  cos01bndlem2 7429  sin01gt0 7435  sin02gt0 7437  infxpidmlem8 7519  infxpidmlem12 7523  infdif 7528  fctop 7610  isnei 7678  cnsscnp 7732  mettri 7777  opnuni 7830  metcnp 7849  metcnss 7860  metcnss2 7861  cmsss 7959  bcthlem7 7967  bcthlem26 7986  bcthlem29 7989  grplactf1o 8061  ring2 8113  sqcn 8298  nmobndi 8398  ubthlem6 8493  efif1lem5 8684  occllem6 9133  osumlem4 9538  stle0 10122  strlem3a 10135  hstrlem3a 10143  hstrb 10149  spansncv2t 10176  h1dat 10232  elghomlem2 10339  ghomf1olem 10352  nndivsub 10379  rcla4devOLD 10389  uninqs 10400  elo 10403  infi1 10405  fiiu2 10436  truni1 10445  hmeogrp 10484  homcard 10485  filintf 10502  fgsb 10503  fisub 10506  fgsb2 10508  rcfpfillem4 10514  ltsubpostb 10543  ltaddpos2tb 10544  trran 10552  trnij 10553  imonclem 10655

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