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

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 29	1 ⊢ (𝜓 → (𝜑 → 𝜒))

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  99  expcom  116  impcom  125  syl5ibcom  155  syl5ibrcom  157  pm5.501  244  impd  254  expd  258  pm3.21  264  imdistanri  446  pm2.24  622  con3rr3  634  expt  658  mtt  686  jaod  718  orel1  726  pm2.62  749  pm2.64  802  pm2.75  810  pm2.61ddc  862  peircedc  915  dcbi  938  pm5.62dc  947  pm4.83dc  953  ccased  967  3impd  1223  3expd  1226  mp3an1i  1341  pclem6  1385  simplbi2com  1455  19.21ht  1595  19.33b2  1643  equtrr  1724  spimeh  1753  cbv1  1759  cbv1v  1761  equvini  1772  sbequ2  1783  ax11e  1810  ax11b  1840  sb6rf  1867  sb56  1900  exmoeudc  2108  moimv  2111  eupickbi  2127  exists2  2142  r19.12  2603  2gencl  2796  3gencl  2797  rspccv  2865  ceqex  2891  mo2icl  2943  mob  2946  euind  2951  reuind  2969  sseq2  3208  nelss  3245  difin  3401  reupick2  3450  uneqdifeqim  3537  difsn  3760  sssnm  3785  preq12b  3801  iinss2  3970  trintssm  4148  sspwb  4250  copsexg  4278  pocl  4339  pofun  4348  sowlin  4356  reusv1  4494  alxfr  4497  ralxfrALT  4503  iunpw  4516  onsucelsucr  4545  reg2exmidlema  4571  en2lp  4591  2optocl  4741  3optocl  4742  ssrel  4752  ssrel2  4754  ssrelrel  4764  relop  4817  xpidtr  5061  trin2  5062  poltletr  5071  xp11m  5109  relcnvtr  5190  iotaval  5231  funmo  5274  fss  5420  f0dom0  5452  fv3  5582  tz6.12c  5589  mpteqb  5653  funfvima  5795  f1veqaeq  5817  isoselem  5868  oprabid  5955  ovg  6063  focdmex  6173  f1o2ndf1  6287  poxp  6291  tposfn2  6325  smoel  6359  tfri3  6426  nnaass  6544  nnmordi  6575  iinerm  6667  2ecoptocl  6683  3ecoptocl  6684  th3qlem2  6698  enm  6880  xpdom2  6891  xpf1o  6906  findcard2  6951  findcard2s  6952  eldju2ndl  7139  updjud  7149  nninfninc  7190  distrnq0  7528  addassnq0  7531  prcdnql  7553  prcunqu  7554  nn0ge2m1nn  9311  nn0le2is012  9410  fzind  9443  nn0ind-raph  9445  zindd  9446  uzin  9636  indstr  9669  xnn0xadd0  9944  icoshft  10067  fzen  10120  uzsubsubfz  10124  elfz1b  10167  elfz0ubfz0  10202  elfz0fzfz0  10203  fz0fzelfz0  10204  elfzmlbp  10209  elfzodifsumelfzo  10279  ssfzo12bi  10303  elfzonelfzo  10308  modfzo0difsn  10489  frec2uzuzd  10496  expcllem  10644  mulexp  10672  leexp2r  10687  bernneq  10754  facdiv  10832  cjexp  11060  absexp  11246  clim2prod  11706  prodfap0  11712  prodfrecap  11713  prodmodc  11745  fprodabs  11783  addmodlteqALT  12026  oddge22np1  12048  nn0enne  12069  nn0o1gt2  12072  gcdneg  12159  dfgcd2  12191  rplpwr  12204  coprmdvds1  12269  qredeq  12274  cncongr1  12281  cncongr2  12282  prm2orodd  12304  nnnn0modprm0  12434  prm23lt5  12442  dvdsprmpweqnn  12515  dvdsprmpweqle  12516  oddprmdvds  12533  prmpwdvds  12534  setsn0fun  12725  isnmgm  13013  sgrpass  13061  insubm  13127  dfgrp3mlem  13240  fiinopn  14250  tgcl  14310  distop  14331  ssnei2  14403  tgcnp  14455  cnpnei  14465  cnmptcom  14544  neibl  14737  rpcxpmul2  15159  fsumdvdsmul  15237  zabsle1  15250  gausslemma2dlem1a  15309  gausslemma2dlem3  15314  lgsquad2lem2  15333  2lgs  15355  bj-nnbist  15400  sumdc2  15455