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-1 5  ax-2 6  ax-mp 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  438  pm2.24  591  con3rr3  603  pm2.52  623  expt  624  mtt  651  jaod  678  orel1  685  pm2.62  708  pm2.64  756  pm2.75  764  pm2.61ddc  802  peircedc  864  dcbi  888  pm5.62dc  897  pm4.83dc  903  ccased  917  3impd  1167  3expd  1170  mp3an1i  1276  pclem6  1320  simplbi2com  1388  19.21ht  1528  19.33b2  1576  equtrr  1654  spimeh  1685  cbv1  1690  equvini  1699  sbequ2  1710  ax11e  1735  ax11b  1765  sb6rf  1792  sb56  1824  exmoeudc  2023  moimv  2026  eupickbi  2042  exists2  2057  r19.12  2497  2gencl  2674  3gencl  2675  rspccv  2741  ceqex  2766  mo2icl  2816  mob  2819  euind  2824  reuind  2842  sseq2  3071  difin  3260  reupick2  3309  uneqdifeqim  3395  difsn  3604  sssnm  3628  preq12b  3644  iinss2  3812  trintssm  3982  sspwb  4076  copsexg  4104  pocl  4163  pofun  4172  sowlin  4180  reusv1  4317  alxfr  4320  ralxfrALT  4326  iunpw  4339  onsucelsucr  4362  reg2exmidlema  4387  en2lp  4407  2optocl  4554  3optocl  4555  ssrel  4565  ssrel2  4567  ssrelrel  4577  relop  4627  xpidtr  4865  trin2  4866  poltletr  4875  xp11m  4913  relcnvtr  4994  iotaval  5035  funmo  5074  fss  5220  f0dom0  5252  fv3  5376  tz6.12c  5383  mpteqb  5443  funfvima  5581  f1veqaeq  5602  isoselem  5653  oprabid  5735  ovg  5841  fornex  5944  f1o2ndf1  6055  poxp  6059  tposfn2  6093  smoel  6127  tfri3  6194  nnaass  6311  nnmordi  6342  iinerm  6431  2ecoptocl  6447  3ecoptocl  6448  th3qlem2  6462  enm  6643  xpdom2  6654  xpf1o  6667  findcard2  6712  findcard2s  6713  eldju2ndl  6872  updjud  6882  distrnq0  7168  addassnq0  7171  prcdnql  7193  prcunqu  7194  nn0ge2m1nn  8889  nn0le2is012  8985  fzind  9018  nn0ind-raph  9020  zindd  9021  uzin  9208  indstr  9238  xnn0xadd0  9491  icoshft  9614  fzen  9664  uzsubsubfz  9668  elfz1b  9711  elfz0ubfz0  9743  elfz0fzfz0  9744  fz0fzelfz0  9745  elfzmlbp  9750  elfzodifsumelfzo  9819  ssfzo12bi  9843  elfzonelfzo  9848  modfzo0difsn  10009  frec2uzuzd  10016  expcllem  10145  mulexp  10173  leexp2r  10188  bernneq  10253  facdiv  10325  cjexp  10506  absexp  10691  addmodlteqALT  11352  oddge22np1  11373  nn0enne  11394  nn0o1gt2  11397  gcdneg  11465  dfgcd2  11495  rplpwr  11508  coprmdvds1  11565  qredeq  11570  cncongr1  11577  cncongr2  11578  prm2orodd  11600  setsn0fun  11778  fiinopn  11953  tgcl  12015  distop  12036  ssnei2  12108  tgcnp  12159  cnpnei  12169  cnmptcom  12248  neibl  12419  sumdc2  12587