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  3492  sssnm  3516  preq12b  3532  iinss2  3700  trint0m  3862  sspwb  3943  copsexg  3972  pocl  4031  pofun  4040  sowlin  4048  reusv1  4156  alxfr  4159  ralxfrALT  4165  iunpw  4177  onsucelsucr  4199  en2lp  4232  2optocl  4360  3optocl  4361  ssrel  4371  ssrel2  4373  ssrelrel  4383  relop  4429  xpidtr  4658  trin2  4659  poltletr  4668  xp11m  4702  relcnvtr  4783  iotaval  4821  funmo  4860  fss  4997  fv3  5140  tz6.12c  5146  mpteqb  5204  funfvima  5333  f1veqaeq  5351  isoselem  5402  oprabid  5480  ovg  5581  fornex  5684  f1o2ndf1  5791  poxp  5794  tposfn2  5822  smoel  5856  tfri3  5894  nnaass  6003  nnmordi  6025  iinerm  6114  2ecoptocl  6130  3ecoptocl  6131  th3qlem2  6145  enm  6230  xpdom2  6241  distrnq0  6441  addassnq0  6444  prcdnql  6466  prcunqu  6467  nn0ge2m1nn  7998  fzind  8109  nn0ind-raph  8111  zindd  8112  uzin  8261  indstr  8292  icoshft  8608  fzen  8657  uzsubsubfz  8661  elfz1b  8702  elfz0ubfz0  8732  elfz0fzfz0  8733  fz0fzelfz0  8734  elfzmlbmOLD  8739  elfzmlbp  8740  elfzodifsumelfzo  8807  ssfzo12bi  8831  elfzonelfzo  8836  frec2uzzd  8847  frec2uzuzd  8849  expcllem  8900  mulexp  8928  leexp2r  8942  bernneq  9002  cjexp  9101
  Copyright terms: Public domain W3C validator