ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  com12 Unicode version

Theorem com12 30
Description: Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
com12  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem com12
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
2 com12.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5com 29 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl11  31  syl5  32  syl6com  35  mpcom  36  syli  37  syl2imc  39  pm2.27  40  syldc  46  pm2.43b  52  syl9r  73  com3r  79  pm2.86i  98  expcom  115  impcom  124  syl5ibcom  154  syl5ibrcom  156  pm5.501  243  impd  252  expd  256  pm3.21  262  imdistanri  442  pm2.24  610  con3rr3  622  expt  646  mtt  674  jaod  706  orel1  714  pm2.62  737  pm2.64  790  pm2.75  798  pm2.61ddc  846  peircedc  899  dcbi  920  pm5.62dc  929  pm4.83dc  935  ccased  949  3impd  1199  3expd  1202  mp3an1i  1308  pclem6  1352  simplbi2com  1420  19.21ht  1560  19.33b2  1608  equtrr  1686  spimeh  1717  cbv1  1722  equvini  1731  sbequ2  1742  ax11e  1768  ax11b  1798  sb6rf  1825  sb56  1857  exmoeudc  2062  moimv  2065  eupickbi  2081  exists2  2096  r19.12  2538  2gencl  2719  3gencl  2720  rspccv  2786  ceqex  2812  mo2icl  2863  mob  2866  euind  2871  reuind  2889  sseq2  3121  nelss  3158  difin  3313  reupick2  3362  uneqdifeqim  3448  difsn  3657  sssnm  3681  preq12b  3697  iinss2  3865  trintssm  4042  sspwb  4138  copsexg  4166  pocl  4225  pofun  4234  sowlin  4242  reusv1  4379  alxfr  4382  ralxfrALT  4388  iunpw  4401  onsucelsucr  4424  reg2exmidlema  4449  en2lp  4469  2optocl  4616  3optocl  4617  ssrel  4627  ssrel2  4629  ssrelrel  4639  relop  4689  xpidtr  4929  trin2  4930  poltletr  4939  xp11m  4977  relcnvtr  5058  iotaval  5099  funmo  5138  fss  5284  f0dom0  5316  fv3  5444  tz6.12c  5451  mpteqb  5511  funfvima  5649  f1veqaeq  5670  isoselem  5721  oprabid  5803  ovg  5909  fornex  6013  f1o2ndf1  6125  poxp  6129  tposfn2  6163  smoel  6197  tfri3  6264  nnaass  6381  nnmordi  6412  iinerm  6501  2ecoptocl  6517  3ecoptocl  6518  th3qlem2  6532  enm  6714  xpdom2  6725  xpf1o  6738  findcard2  6783  findcard2s  6784  eldju2ndl  6957  updjud  6967  distrnq0  7279  addassnq0  7282  prcdnql  7304  prcunqu  7305  nn0ge2m1nn  9049  nn0le2is012  9145  fzind  9178  nn0ind-raph  9180  zindd  9181  uzin  9370  indstr  9400  xnn0xadd0  9662  icoshft  9785  fzen  9835  uzsubsubfz  9839  elfz1b  9882  elfz0ubfz0  9914  elfz0fzfz0  9915  fz0fzelfz0  9916  elfzmlbp  9921  elfzodifsumelfzo  9990  ssfzo12bi  10014  elfzonelfzo  10019  modfzo0difsn  10180  frec2uzuzd  10187  expcllem  10316  mulexp  10344  leexp2r  10359  bernneq  10424  facdiv  10496  cjexp  10677  absexp  10863  clim2prod  11320  prodfap0  11326  prodfrecap  11327  prodmodc  11359  addmodlteqALT  11568  oddge22np1  11589  nn0enne  11610  nn0o1gt2  11613  gcdneg  11681  dfgcd2  11713  rplpwr  11726  coprmdvds1  11783  qredeq  11788  cncongr1  11795  cncongr2  11796  prm2orodd  11818  setsn0fun  12010  fiinopn  12185  tgcl  12247  distop  12268  ssnei2  12340  tgcnp  12392  cnpnei  12402  cnmptcom  12481  neibl  12674  bj-nnbist  13012  sumdc2  13065
  Copyright terms: Public domain W3C validator