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

Theorem com12 27
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 26 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:  syl5  28  syl6com  31  mpcom  32  syli  33  pm2.27  35  pm2.43b  46  syl9r  67  com3r  73  pm2.86i  92  expcom  109  impcom  116  syl5ibcom  144  syl5ibrcom  146  pm5.501  233  impd  242  expd  245  pm3.21  251  imdistanri  420  pm2.24  551  con3rr3  563  pm2.52  582  expt  583  mtt  610  jaod  637  orel1  644  pm2.62  667  pm2.64  714  pm2.75  722  pm2.61ddc  758  peircedc  820  dcbi  844  pm5.62dc  852  pm4.83dc  858  ccased  872  3impd  1118  3expd  1121  mp3an1i  1225  pclem6  1265  simplbi2com  1333  19.21ht  1473  19.33b2  1520  equtrr  1596  spimeh  1627  cbv1  1632  equvini  1641  sbequ2  1652  ax11e  1677  ax11b  1707  sb6rf  1733  sb56  1765  exmoeudc  1963  moimv  1966  eupickbi  1982  exists2  1997  r19.12  2422  2gencl  2587  3gencl  2588  rspccv  2653  ceqex  2671  mo2icl  2720  mob  2723  euind  2728  reuind  2744  sseq2  2967  difin  3174  reupick2  3223  uneqdifeqim  3308  difsn  3501  sssnm  3525  preq12b  3541  iinss2  3709  trint0m  3871  sspwb  3952  copsexg  3981  pocl  4040  pofun  4049  sowlin  4057  reusv1  4190  alxfr  4193  ralxfrALT  4199  iunpw  4211  onsucelsucr  4234  reg2exmidlema  4259  en2lp  4278  2optocl  4417  3optocl  4418  ssrel  4428  ssrel2  4430  ssrelrel  4440  relop  4486  xpidtr  4715  trin2  4716  poltletr  4725  xp11m  4759  relcnvtr  4840  iotaval  4878  funmo  4917  fss  5054  fv3  5197  tz6.12c  5203  mpteqb  5261  funfvima  5390  f1veqaeq  5408  isoselem  5459  oprabid  5537  ovg  5639  fornex  5742  f1o2ndf1  5849  poxp  5853  tposfn2  5881  smoel  5915  tfri3  5953  nnaass  6064  nnmordi  6089  iinerm  6178  2ecoptocl  6194  3ecoptocl  6195  th3qlem2  6209  enm  6294  xpdom2  6305  findcard2  6346  findcard2s  6347  distrnq0  6557  addassnq0  6560  prcdnql  6582  prcunqu  6583  nn0ge2m1nn  8242  fzind  8353  nn0ind-raph  8355  zindd  8356  uzin  8505  indstr  8536  icoshft  8858  fzen  8907  uzsubsubfz  8911  elfz1b  8952  elfz0ubfz0  8982  elfz0fzfz0  8983  fz0fzelfz0  8984  elfzmlbmOLD  8989  elfzmlbp  8990  elfzodifsumelfzo  9057  ssfzo12bi  9081  elfzonelfzo  9086  frec2uzzd  9186  frec2uzuzd  9188  expcllem  9266  mulexp  9294  leexp2r  9308  bernneq  9369  cjexp  9493  absexp  9675
  Copyright terms: Public domain W3C validator