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  pm2.27  39  syldc  45  pm2.43b  51  syl9r  72  com3r  78  pm2.86i  97  expcom  114  impcom  123  syl5ibcom  153  syl5ibrcom  155  pm5.501  242  impd  251  expd  254  pm3.21  260  imdistanri  435  pm2.24  584  con3rr3  596  pm2.52  615  expt  616  mtt  643  jaod  670  orel1  677  pm2.62  700  pm2.64  748  pm2.75  756  pm2.61ddc  794  peircedc  856  dcbi  880  pm5.62dc  889  pm4.83dc  895  ccased  909  3impd  1155  3expd  1158  mp3an1i  1264  pclem6  1308  simplbi2com  1376  19.21ht  1516  19.33b2  1563  equtrr  1640  spimeh  1671  cbv1  1676  equvini  1685  sbequ2  1696  ax11e  1721  ax11b  1751  sb6rf  1778  sb56  1810  exmoeudc  2008  moimv  2011  eupickbi  2027  exists2  2042  r19.12  2474  2gencl  2646  3gencl  2647  rspccv  2712  ceqex  2735  mo2icl  2785  mob  2788  euind  2793  reuind  2809  sseq2  3037  difin  3225  reupick2  3274  uneqdifeqim  3355  difsn  3557  sssnm  3581  preq12b  3597  iinss2  3765  trintssm  3927  sspwb  4017  copsexg  4045  pocl  4104  pofun  4113  sowlin  4121  reusv1  4254  alxfr  4257  ralxfrALT  4263  iunpw  4275  onsucelsucr  4298  reg2exmidlema  4323  en2lp  4343  2optocl  4483  3optocl  4484  ssrel  4494  ssrel2  4496  ssrelrel  4506  relop  4554  xpidtr  4789  trin2  4790  poltletr  4799  xp11m  4835  relcnvtr  4916  iotaval  4957  funmo  4996  fss  5136  f0dom0  5167  fv3  5291  tz6.12c  5297  mpteqb  5356  funfvima  5487  f1veqaeq  5509  isoselem  5560  oprabid  5638  ovg  5740  fornex  5843  f1o2ndf1  5950  poxp  5954  tposfn2  5985  smoel  6019  tfri3  6086  nnaass  6200  nnmordi  6227  iinerm  6316  2ecoptocl  6332  3ecoptocl  6333  th3qlem2  6347  enm  6488  xpdom2  6499  xpf1o  6512  findcard2  6557  findcard2s  6558  eldju2ndl  6707  updjud  6717  distrnq0  6962  addassnq0  6965  prcdnql  6987  prcunqu  6988  nn0ge2m1nn  8666  fzind  8794  nn0ind-raph  8796  zindd  8797  uzin  8983  indstr  9013  icoshft  9339  fzen  9389  uzsubsubfz  9393  elfz1b  9434  elfz0ubfz0  9464  elfz0fzfz0  9465  fz0fzelfz0  9466  elfzmlbp  9471  elfzodifsumelfzo  9540  ssfzo12bi  9564  elfzonelfzo  9569  modfzo0difsn  9730  frec2uzuzd  9737  expcllem  9865  mulexp  9893  leexp2r  9908  bernneq  9971  facdiv  10043  cjexp  10223  absexp  10408  addmodlteqALT  10742  oddge22np1  10763  nn0enne  10784  nn0o1gt2  10787  gcdneg  10855  dfgcd2  10885  rplpwr  10898  coprmdvds1  10955  qredeq  10960  cncongr1  10967  cncongr2  10968  prm2orodd  10990  sumdc2  11144