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  626  con3rr3  638  expt  663  mtt  692  jaod  725  orel1  733  pm2.62  756  pm2.64  809  pm2.75  817  pm2.61ddc  869  peircedc  922  dcbi  945  pm5.62dc  954  pm4.83dc  960  ccased  974  3impd  1248  3expd  1251  syldbl2  1329  mp3an1i  1367  pclem6  1419  simplbi2com  1490  19.21ht  1630  19.33b2  1678  equtrr  1758  spimeh  1788  cbv1  1794  cbv1v  1796  equvini  1807  sbequ2  1818  ax11e  1845  ax11b  1875  sb6rf  1902  sb56  1936  exmoeudc  2146  moimv  2149  eupickbi  2165  exists2  2180  r19.12  2651  2gencl  2849  3gencl  2850  vtocl4ga  2889  rspccv  2920  ceqex  2947  mo2icl  2999  mob  3002  euind  3007  reuind  3025  sseq2  3266  nelss  3303  difin  3462  reupick2  3511  uneqdifeqim  3599  sspw  3687  difsn  3836  ssprsseq  3861  sssnm  3863  preq12b  3879  iinss2  4049  trintssm  4229  sspwb  4337  copsexg  4365  pocl  4429  pofun  4438  sowlin  4446  reusv1  4584  alxfr  4587  ralxfrALT  4593  iunpw  4606  onsucelsucr  4635  reg2exmidlema  4661  en2lp  4681  2optocl  4832  3optocl  4833  ssrel  4843  ssrel2  4845  ssrelrel  4855  relop  4910  xpidtr  5158  trin2  5159  poltletr  5168  xp11m  5206  relcnvtr  5287  iotaval  5329  funmo  5372  fundif  5405  fss  5526  f0dom0  5566  fv3  5698  tz6.12c  5705  mpteqb  5773  funfvima  5923  f1veqaeq  5948  isoselem  5999  oprabid  6090  ovg  6201  focdmex  6317  f1o2ndf1  6437  poxp  6441  tposfn2  6510  smoel  6544  tfri3  6611  nnaass  6731  nnmordi  6762  iinerm  6854  2ecoptocl  6870  3ecoptocl  6871  th3qlem2  6885  enm  7084  xpdom2  7095  xpf1o  7110  findcard2  7159  findcard2s  7160  suppeqfsuppbi  7261  eldju2ndl  7376  updjud  7386  nninfninc  7427  distrnq0  7790  addassnq0  7793  prcdnql  7815  prcunqu  7816  nn0ge2m1nn  9580  nn0le2is012  9681  fzind  9714  nn0ind-raph  9716  zindd  9717  uzin  9908  indstr  9946  xnn0xadd0  10222  icoshft  10345  fzen  10400  uzsubsubfz  10404  elfz1b  10449  elfz0ubfz0  10484  elfz0fzfz0  10485  fz0fzelfz0  10486  elfzmlbp  10491  elfzodifsumelfzo  10571  ssfzo12bi  10595  elfzonelfzo  10600  modfzo0difsn  10784  frec2uzuzd  10791  expcllem  10939  mulexp  10967  leexp2r  10982  bernneq  11050  facdiv  11128  fundm2domnop0  11248  ccatsymb  11318  swrdnd  11379  swrdswrdlem  11424  swrdswrd  11425  pfxccatin12lem2a  11447  pfxccatin12lem1  11448  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12lem3  11452  pfxccat3  11454  swrdccat  11455  swrdccat3blem  11459  cjexp  11606  absexp  11792  clim2prod  12253  prodfap0  12259  prodfrecap  12260  prodmodc  12292  fprodabs  12330  addmodlteqALT  12573  oddge22np1  12595  nn0enne  12616  nn0o1gt2  12619  gcdneg  12706  dfgcd2  12738  rplpwr  12751  coprmdvds1  12816  qredeq  12821  cncongr1  12828  cncongr2  12829  prm2orodd  12851  nnnn0modprm0  12981  prm23lt5  12989  dvdsprmpweqnn  13062  dvdsprmpweqle  13063  oddprmdvds  13080  prmpwdvds  13081  setsn0fun  13336  isnmgm  13626  sgrpass  13674  insubm  13743  dfgrp3mlem  13856  fiinopn  14998  tgcl  15058  distop  15079  ssnei2  15151  tgcnp  15203  cnpnei  15213  cnmptcom  15292  neibl  15485  rpcxpmul2  15907  fsumdvdsmul  15988  zabsle1  16001  gausslemma2dlem1a  16060  gausslemma2dlem3  16065  lgsquad2lem2  16084  2lgs  16106  umgrnloop  16240  upgrpredgv  16270  upgredgpr  16273  wlkl1loop  16482  upgriswlkdc  16484  upgrwlkvtxedg  16488  uspgr2wlkeq  16489  wlkv0  16493  wlkres  16503  clwwlkccatlem  16524  loopclwwlkn1b  16543  umgr2cwwk2dif  16548  clwwlknonex2lem2  16562  clwwlknonex2  16563  eupth2lem3lem4fi  16597  depindlem2  16631  bj-nnbist  16655  sumdc2  16710