ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  com12 GIF 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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
com12 (𝜓 → (𝜑𝜒))

Proof of Theorem com12
StepHypRef Expression
1 id 19 . 2 (𝜓𝜓)
2 com12.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5com 29 1 (𝜓 → (𝜑𝜒))
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  443  pm2.24  611  con3rr3  623  expt  647  mtt  675  jaod  707  orel1  715  pm2.62  738  pm2.64  791  pm2.75  799  pm2.61ddc  847  peircedc  900  dcbi  921  pm5.62dc  930  pm4.83dc  936  ccased  950  3impd  1200  3expd  1203  mp3an1i  1309  pclem6  1353  simplbi2com  1421  19.21ht  1561  19.33b2  1609  equtrr  1687  spimeh  1718  cbv1  1723  equvini  1732  sbequ2  1743  ax11e  1769  ax11b  1799  sb6rf  1826  sb56  1858  exmoeudc  2063  moimv  2066  eupickbi  2082  exists2  2097  r19.12  2541  2gencl  2722  3gencl  2723  rspccv  2789  ceqex  2815  mo2icl  2866  mob  2869  euind  2874  reuind  2892  sseq2  3125  nelss  3162  difin  3317  reupick2  3366  uneqdifeqim  3452  difsn  3664  sssnm  3688  preq12b  3704  iinss2  3872  trintssm  4049  sspwb  4145  copsexg  4173  pocl  4232  pofun  4241  sowlin  4249  reusv1  4386  alxfr  4389  ralxfrALT  4395  iunpw  4408  onsucelsucr  4431  reg2exmidlema  4456  en2lp  4476  2optocl  4623  3optocl  4624  ssrel  4634  ssrel2  4636  ssrelrel  4646  relop  4696  xpidtr  4936  trin2  4937  poltletr  4946  xp11m  4984  relcnvtr  5065  iotaval  5106  funmo  5145  fss  5291  f0dom0  5323  fv3  5451  tz6.12c  5458  mpteqb  5518  funfvima  5656  f1veqaeq  5677  isoselem  5728  oprabid  5810  ovg  5916  fornex  6020  f1o2ndf1  6132  poxp  6136  tposfn2  6170  smoel  6204  tfri3  6271  nnaass  6388  nnmordi  6419  iinerm  6508  2ecoptocl  6524  3ecoptocl  6525  th3qlem2  6539  enm  6721  xpdom2  6732  xpf1o  6745  findcard2  6790  findcard2s  6791  eldju2ndl  6964  updjud  6974  distrnq0  7290  addassnq0  7293  prcdnql  7315  prcunqu  7316  nn0ge2m1nn  9060  nn0le2is012  9156  fzind  9189  nn0ind-raph  9191  zindd  9192  uzin  9381  indstr  9414  xnn0xadd0  9679  icoshft  9802  fzen  9853  uzsubsubfz  9857  elfz1b  9900  elfz0ubfz0  9932  elfz0fzfz0  9933  fz0fzelfz0  9934  elfzmlbp  9939  elfzodifsumelfzo  10008  ssfzo12bi  10032  elfzonelfzo  10037  modfzo0difsn  10198  frec2uzuzd  10205  expcllem  10334  mulexp  10362  leexp2r  10377  bernneq  10442  facdiv  10515  cjexp  10696  absexp  10882  clim2prod  11339  prodfap0  11345  prodfrecap  11346  prodmodc  11378  addmodlteqALT  11591  oddge22np1  11612  nn0enne  11633  nn0o1gt2  11636  gcdneg  11704  dfgcd2  11736  rplpwr  11749  coprmdvds1  11806  qredeq  11811  cncongr1  11818  cncongr2  11819  prm2orodd  11841  setsn0fun  12033  fiinopn  12208  tgcl  12270  distop  12291  ssnei2  12363  tgcnp  12415  cnpnei  12425  cnmptcom  12504  neibl  12697  bj-nnbist  13122  sumdc2  13175
  Copyright terms: Public domain W3C validator