ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  com12 Structured version   GIF 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 (φ → (ψχ))
Assertion
Ref Expression
com12 (ψ → (φχ))

Proof of Theorem com12
StepHypRef Expression
1 id 19 . 2 (ψψ)
2 com12.1 . 2 (φ → (ψχ))
31, 2syl5com 26 1 (ψ → (φχ))
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  562  pm2.52  581  expt  582  mtt  609  jaod  636  orel1  643  pm2.62  666  pm2.64  713  pm2.75  721  pm2.61ddc  757  peircedc  819  dcbi  843  pm5.62dc  851  pm4.83dc  857  ccased  871  3impd  1117  3expd  1120  mp3an1i  1224  pclem6  1264  simplbi2com  1330  19.21ht  1470  19.33b2  1517  equtrr  1593  spimeh  1624  cbv1  1629  equvini  1638  sbequ2  1649  ax11e  1674  ax11b  1704  sb6rf  1730  sb56  1762  exmoeudc  1960  moimv  1963  eupickbi  1979  exists2  1994  r19.12  2416  2gencl  2581  3gencl  2582  rspccv  2647  ceqex  2665  mo2icl  2714  mob  2717  euind  2722  reuind  2738  sseq2  2961  difin  3168  reupick2  3217  uneqdifeqim  3302  difsn  3491  sssnm  3515  preq12b  3531  iinss2  3699  trint0m  3861  sspwb  3942  copsexg  3971  pocl  4030  pofun  4039  sowlin  4047  reusv1  4155  alxfr  4158  ralxfrALT  4164  iunpw  4176  onsucelsucr  4198  en2lp  4231  2optocl  4359  3optocl  4360  ssrel  4370  ssrel2  4372  ssrelrel  4382  relop  4428  xpidtr  4657  trin2  4658  poltletr  4667  xp11m  4701  relcnvtr  4782  iotaval  4820  funmo  4858  fss  4995  fv3  5138  tz6.12c  5144  mpteqb  5202  funfvima  5331  f1veqaeq  5349  isoselem  5400  oprabid  5477  ovg  5578  fornex  5681  f1o2ndf1  5788  poxp  5791  tposfn2  5819  smoel  5853  tfri3  5891  nnaass  5996  nnmordi  6018  iinerm  6107  2ecoptocl  6123  3ecoptocl  6124  th3qlem2  6138  enm  6223  xpdom2  6234  distrnq0  6434  addassnq0  6437  prcdnql  6459  prcunqu  6460  nn0ge2m1nn  7968  fzind  8078  nn0ind-raph  8080  zindd  8081  uzin  8230  indstr  8261  icoshft  8576  fzen  8623  uzsubsubfz  8627  elfz1b  8668  elfz0ubfz0  8698  elfz0fzfz0  8699  fz0fzelfz0  8700  elfzmlbmOLD  8705  elfzmlbp  8706  elfzodifsumelfzo  8773  ssfzo12bi  8797  elfzonelfzo  8802  frec2uzzd  8813  frec2uzuzd  8815
  Copyright terms: Public domain W3C validator