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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syl11  31  syl5  32  syl6com  35  mpcom  36  syli  37  pm2.27  39  syldc  45  pm2.43b  51  syl9r  72  com3r  78  pm2.86i  97  expcom  114  impcom  123  syl5ibcom  153  syl5ibrcom  155  pm5.501  242  impd  251  expd  254  pm3.21  260  imdistanri  435  pm2.24  586  con3rr3  598  pm2.52  617  expt  618  mtt  645  jaod  672  orel1  679  pm2.62  702  pm2.64  750  pm2.75  758  pm2.61ddc  796  peircedc  858  dcbi  882  pm5.62dc  891  pm4.83dc  897  ccased  911  3impd  1157  3expd  1160  mp3an1i  1266  pclem6  1310  simplbi2com  1378  19.21ht  1518  19.33b2  1565  equtrr  1643  spimeh  1674  cbv1  1679  equvini  1688  sbequ2  1699  ax11e  1724  ax11b  1754  sb6rf  1781  sb56  1813  exmoeudc  2011  moimv  2014  eupickbi  2030  exists2  2045  r19.12  2478  2gencl  2652  3gencl  2653  rspccv  2719  ceqex  2742  mo2icl  2792  mob  2795  euind  2800  reuind  2818  sseq2  3046  difin  3234  reupick2  3283  uneqdifeqim  3364  difsn  3569  sssnm  3593  preq12b  3609  iinss2  3777  trintssm  3944  sspwb  4034  copsexg  4062  pocl  4121  pofun  4130  sowlin  4138  reusv1  4271  alxfr  4274  ralxfrALT  4280  iunpw  4292  onsucelsucr  4315  reg2exmidlema  4340  en2lp  4360  2optocl  4503  3optocl  4504  ssrel  4514  ssrel2  4516  ssrelrel  4526  relop  4574  xpidtr  4809  trin2  4810  poltletr  4819  xp11m  4856  relcnvtr  4937  iotaval  4978  funmo  5017  fss  5157  f0dom0  5188  fv3  5312  tz6.12c  5318  mpteqb  5377  funfvima  5508  f1veqaeq  5530  isoselem  5581  oprabid  5663  ovg  5765  fornex  5868  f1o2ndf1  5975  poxp  5979  tposfn2  6013  smoel  6047  tfri3  6114  nnaass  6228  nnmordi  6255  iinerm  6344  2ecoptocl  6360  3ecoptocl  6361  th3qlem2  6375  enm  6516  xpdom2  6527  xpf1o  6540  findcard2  6585  findcard2s  6586  eldju2ndl  6742  updjud  6752  distrnq0  6997  addassnq0  7000  prcdnql  7022  prcunqu  7023  nn0ge2m1nn  8703  fzind  8831  nn0ind-raph  8833  zindd  8834  uzin  9020  indstr  9050  icoshft  9376  fzen  9426  uzsubsubfz  9430  elfz1b  9471  elfz0ubfz0  9501  elfz0fzfz0  9502  fz0fzelfz0  9503  elfzmlbp  9508  elfzodifsumelfzo  9577  ssfzo12bi  9601  elfzonelfzo  9606  modfzo0difsn  9767  frec2uzuzd  9774  expcllem  9930  mulexp  9958  leexp2r  9973  bernneq  10038  facdiv  10110  cjexp  10291  absexp  10476  addmodlteqALT  10940  oddge22np1  10961  nn0enne  10982  nn0o1gt2  10985  gcdneg  11053  dfgcd2  11083  rplpwr  11096  coprmdvds1  11153  qredeq  11158  cncongr1  11165  cncongr2  11166  prm2orodd  11188  sumdc2  11343
  Copyright terms: Public domain W3C validator