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  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  851  peircedc  904  dcbi  925  pm5.62dc  934  pm4.83dc  940  ccased  954  3impd  1210  3expd  1213  mp3an1i  1319  pclem6  1363  simplbi2com  1431  19.21ht  1568  19.33b2  1616  equtrr  1697  spimeh  1726  cbv1  1732  cbv1v  1734  equvini  1745  sbequ2  1756  ax11e  1783  ax11b  1813  sb6rf  1840  sb56  1872  exmoeudc  2076  moimv  2079  eupickbi  2095  exists2  2110  r19.12  2570  2gencl  2754  3gencl  2755  rspccv  2822  ceqex  2848  mo2icl  2900  mob  2903  euind  2908  reuind  2926  sseq2  3161  nelss  3198  difin  3354  reupick2  3403  uneqdifeqim  3489  difsn  3704  sssnm  3728  preq12b  3744  iinss2  3912  trintssm  4090  sspwb  4188  copsexg  4216  pocl  4275  pofun  4284  sowlin  4292  reusv1  4430  alxfr  4433  ralxfrALT  4439  iunpw  4452  onsucelsucr  4479  reg2exmidlema  4505  en2lp  4525  2optocl  4675  3optocl  4676  ssrel  4686  ssrel2  4688  ssrelrel  4698  relop  4748  xpidtr  4988  trin2  4989  poltletr  4998  xp11m  5036  relcnvtr  5117  iotaval  5158  funmo  5197  fss  5343  f0dom0  5375  fv3  5503  tz6.12c  5510  mpteqb  5570  funfvima  5710  f1veqaeq  5731  isoselem  5782  oprabid  5865  ovg  5971  fornex  6075  f1o2ndf1  6187  poxp  6191  tposfn2  6225  smoel  6259  tfri3  6326  nnaass  6444  nnmordi  6475  iinerm  6564  2ecoptocl  6580  3ecoptocl  6581  th3qlem2  6595  enm  6777  xpdom2  6788  xpf1o  6801  findcard2  6846  findcard2s  6847  eldju2ndl  7028  updjud  7038  distrnq0  7391  addassnq0  7394  prcdnql  7416  prcunqu  7417  nn0ge2m1nn  9165  nn0le2is012  9264  fzind  9297  nn0ind-raph  9299  zindd  9300  uzin  9489  indstr  9522  xnn0xadd0  9794  icoshft  9917  fzen  9968  uzsubsubfz  9972  elfz1b  10015  elfz0ubfz0  10050  elfz0fzfz0  10051  fz0fzelfz0  10052  elfzmlbp  10057  elfzodifsumelfzo  10126  ssfzo12bi  10150  elfzonelfzo  10155  modfzo0difsn  10320  frec2uzuzd  10327  expcllem  10456  mulexp  10484  leexp2r  10499  bernneq  10564  facdiv  10640  cjexp  10821  absexp  11007  clim2prod  11466  prodfap0  11472  prodfrecap  11473  prodmodc  11505  fprodabs  11543  addmodlteqALT  11782  oddge22np1  11803  nn0enne  11824  nn0o1gt2  11827  gcdneg  11900  dfgcd2  11932  rplpwr  11945  coprmdvds1  12002  qredeq  12007  cncongr1  12014  cncongr2  12015  prm2orodd  12037  nnnn0modprm0  12164  prm23lt5  12172  dvdsprmpweqnn  12244  dvdsprmpweqle  12245  oddprmdvds  12261  setsn0fun  12368  fiinopn  12543  tgcl  12605  distop  12626  ssnei2  12698  tgcnp  12750  cnpnei  12760  cnmptcom  12839  neibl  13032  bj-nnbist  13460  sumdc2  13515