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  926  pm5.62dc  935  pm4.83dc  941  ccased  955  3impd  1211  3expd  1214  mp3an1i  1320  pclem6  1364  simplbi2com  1432  19.21ht  1569  19.33b2  1617  equtrr  1698  spimeh  1727  cbv1  1733  cbv1v  1735  equvini  1746  sbequ2  1757  ax11e  1784  ax11b  1814  sb6rf  1841  sb56  1873  exmoeudc  2077  moimv  2080  eupickbi  2096  exists2  2111  r19.12  2572  2gencl  2759  3gencl  2760  rspccv  2827  ceqex  2853  mo2icl  2905  mob  2908  euind  2913  reuind  2931  sseq2  3166  nelss  3203  difin  3359  reupick2  3408  uneqdifeqim  3494  difsn  3710  sssnm  3734  preq12b  3750  iinss2  3918  trintssm  4096  sspwb  4194  copsexg  4222  pocl  4281  pofun  4290  sowlin  4298  reusv1  4436  alxfr  4439  ralxfrALT  4445  iunpw  4458  onsucelsucr  4485  reg2exmidlema  4511  en2lp  4531  2optocl  4681  3optocl  4682  ssrel  4692  ssrel2  4694  ssrelrel  4704  relop  4754  xpidtr  4994  trin2  4995  poltletr  5004  xp11m  5042  relcnvtr  5123  iotaval  5164  funmo  5203  fss  5349  f0dom0  5381  fv3  5509  tz6.12c  5516  mpteqb  5576  funfvima  5716  f1veqaeq  5737  isoselem  5788  oprabid  5874  ovg  5980  fornex  6083  f1o2ndf1  6196  poxp  6200  tposfn2  6234  smoel  6268  tfri3  6335  nnaass  6453  nnmordi  6484  iinerm  6573  2ecoptocl  6589  3ecoptocl  6590  th3qlem2  6604  enm  6786  xpdom2  6797  xpf1o  6810  findcard2  6855  findcard2s  6856  eldju2ndl  7037  updjud  7047  distrnq0  7400  addassnq0  7403  prcdnql  7425  prcunqu  7426  nn0ge2m1nn  9174  nn0le2is012  9273  fzind  9306  nn0ind-raph  9308  zindd  9309  uzin  9498  indstr  9531  xnn0xadd0  9803  icoshft  9926  fzen  9978  uzsubsubfz  9982  elfz1b  10025  elfz0ubfz0  10060  elfz0fzfz0  10061  fz0fzelfz0  10062  elfzmlbp  10067  elfzodifsumelfzo  10136  ssfzo12bi  10160  elfzonelfzo  10165  modfzo0difsn  10330  frec2uzuzd  10337  expcllem  10466  mulexp  10494  leexp2r  10509  bernneq  10575  facdiv  10651  cjexp  10835  absexp  11021  clim2prod  11480  prodfap0  11486  prodfrecap  11487  prodmodc  11519  fprodabs  11557  addmodlteqALT  11797  oddge22np1  11818  nn0enne  11839  nn0o1gt2  11842  gcdneg  11915  dfgcd2  11947  rplpwr  11960  coprmdvds1  12023  qredeq  12028  cncongr1  12035  cncongr2  12036  prm2orodd  12058  nnnn0modprm0  12187  prm23lt5  12195  dvdsprmpweqnn  12267  dvdsprmpweqle  12268  oddprmdvds  12284  prmpwdvds  12285  setsn0fun  12431  isnmgm  12591  fiinopn  12642  tgcl  12704  distop  12725  ssnei2  12797  tgcnp  12849  cnpnei  12859  cnmptcom  12938  neibl  13131  zabsle1  13540  bj-nnbist  13625  sumdc2  13680