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  434  pm2.24  583  con3rr3  595  pm2.52  614  expt  615  mtt  642  jaod  669  orel1  676  pm2.62  699  pm2.64  747  pm2.75  755  pm2.61ddc  791  peircedc  853  dcbi  877  pm5.62dc  886  pm4.83dc  892  ccased  906  3impd  1152  3expd  1155  mp3an1i  1261  pclem6  1305  simplbi2com  1373  19.21ht  1513  19.33b2  1560  equtrr  1636  spimeh  1667  cbv1  1672  equvini  1681  sbequ2  1692  ax11e  1717  ax11b  1747  sb6rf  1774  sb56  1806  exmoeudc  2004  moimv  2007  eupickbi  2023  exists2  2038  r19.12  2466  2gencl  2632  3gencl  2633  rspccv  2698  ceqex  2722  mo2icl  2771  mob  2774  euind  2779  reuind  2795  sseq2  3021  difin  3201  reupick2  3250  uneqdifeqim  3328  difsn  3523  sssnm  3546  preq12b  3562  iinss2  3730  trintssm  3891  sspwb  3971  copsexg  3999  pocl  4058  pofun  4067  sowlin  4075  reusv1  4208  alxfr  4211  ralxfrALT  4217  iunpw  4229  onsucelsucr  4252  reg2exmidlema  4277  en2lp  4297  2optocl  4435  3optocl  4436  ssrel  4446  ssrel2  4448  ssrelrel  4458  relop  4504  xpidtr  4735  trin2  4736  poltletr  4745  xp11m  4779  relcnvtr  4860  iotaval  4898  funmo  4937  fss  5074  fv3  5218  tz6.12c  5224  mpteqb  5282  funfvima  5411  f1veqaeq  5429  isoselem  5479  oprabid  5557  ovg  5659  fornex  5762  f1o2ndf1  5869  poxp  5873  tposfn2  5904  smoel  5938  tfri3  5976  nnaass  6087  nnmordi  6112  iinerm  6201  2ecoptocl  6217  3ecoptocl  6218  th3qlem2  6232  enm  6317  xpdom2  6328  findcard2  6373  findcard2s  6374  distrnq0  6649  addassnq0  6652  prcdnql  6674  prcunqu  6675  nn0ge2m1nn  8348  fzind  8462  nn0ind-raph  8464  zindd  8465  uzin  8651  indstr  8681  icoshft  9012  fzen  9062  uzsubsubfz  9066  elfz1b  9107  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  elfzmlbp  9143  elfzodifsumelfzo  9210  ssfzo12bi  9234  elfzonelfzo  9239  modfzo0difsn  9397  frec2uzzd  9402  frec2uzuzd  9404  expcllem  9487  mulexp  9515  leexp2r  9530  bernneq  9593  facdiv  9665  cjexp  9780  absexp  9965  addmodlteqALT  10259  oddge22np1  10281  nn0enne  10302  nn0o1gt2  10305  gcdneg  10373  dfgcd2  10403  rplpwr  10416  coprmdvds1  10473  qredeq  10478  cncongr1  10485  cncongr2  10486  prm2orodd  10508