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-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  584  con3rr3  596  pm2.52  615  expt  616  mtt  643  jaod  670  orel1  677  pm2.62  700  pm2.64  748  pm2.75  756  pm2.61ddc  792  peircedc  854  dcbi  878  pm5.62dc  887  pm4.83dc  893  ccased  907  3impd  1153  3expd  1156  mp3an1i  1262  pclem6  1306  simplbi2com  1374  19.21ht  1514  19.33b2  1561  equtrr  1637  spimeh  1668  cbv1  1673  equvini  1682  sbequ2  1693  ax11e  1718  ax11b  1748  sb6rf  1775  sb56  1807  exmoeudc  2005  moimv  2008  eupickbi  2024  exists2  2039  r19.12  2467  2gencl  2633  3gencl  2634  rspccv  2699  ceqex  2723  mo2icl  2772  mob  2775  euind  2780  reuind  2796  sseq2  3022  difin  3208  reupick2  3257  uneqdifeqim  3335  difsn  3531  sssnm  3554  preq12b  3570  iinss2  3738  trintssm  3899  sspwb  3979  copsexg  4007  pocl  4066  pofun  4075  sowlin  4083  reusv1  4216  alxfr  4219  ralxfrALT  4225  iunpw  4237  onsucelsucr  4260  reg2exmidlema  4285  en2lp  4305  2optocl  4443  3optocl  4444  ssrel  4454  ssrel2  4456  ssrelrel  4466  relop  4514  xpidtr  4745  trin2  4746  poltletr  4755  xp11m  4789  relcnvtr  4870  iotaval  4908  funmo  4947  fss  5085  fv3  5229  tz6.12c  5235  mpteqb  5293  funfvima  5422  f1veqaeq  5440  isoselem  5490  oprabid  5568  ovg  5670  fornex  5773  f1o2ndf1  5880  poxp  5884  tposfn2  5915  smoel  5949  tfri3  6016  nnaass  6129  nnmordi  6155  iinerm  6244  2ecoptocl  6260  3ecoptocl  6261  th3qlem2  6275  enm  6364  xpdom2  6375  xpf1o  6385  findcard2  6423  findcard2s  6424  distrnq0  6711  addassnq0  6714  prcdnql  6736  prcunqu  6737  nn0ge2m1nn  8415  fzind  8543  nn0ind-raph  8545  zindd  8546  uzin  8732  indstr  8762  icoshft  9088  fzen  9138  uzsubsubfz  9142  elfz1b  9183  elfz0ubfz0  9213  elfz0fzfz0  9214  fz0fzelfz0  9215  elfzmlbp  9220  elfzodifsumelfzo  9287  ssfzo12bi  9311  elfzonelfzo  9316  modfzo0difsn  9477  frec2uzuzd  9484  expcllem  9584  mulexp  9612  leexp2r  9627  bernneq  9690  facdiv  9762  cjexp  9918  absexp  10103  addmodlteqALT  10404  oddge22np1  10425  nn0enne  10446  nn0o1gt2  10449  gcdneg  10517  dfgcd2  10547  rplpwr  10560  coprmdvds1  10617  qredeq  10622  cncongr1  10629  cncongr2  10630  prm2orodd  10652  sumdc2  10787
  Copyright terms: Public domain W3C validator