Theorem com12 27

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 26	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:  syl5  28  syl6com  31  mpcom  32  syli  33  pm2.27  35  pm2.43b  46  syl9r  67  com3r  73  pm2.86i  92  pm2.24  101  con3rr3  128  expt  148  jad  154  pm2.61  163  syl5ibcom  211  syl5ibrcom  213  pm5.501  330  jaod  369  orel1  371  pm2.62  398  impcom  419  imp3a  420  expcom  424  exp3a  425  pm3.21  435  imdistanri  672  pm2.64  764  pm2.75  822  ccased  913  dedlem0b  919  3impd  1165  3expd  1168  mp3an1i  1270  simplbi2com  1374  meredith  1404  sbequ2  1650  equtrr  1683  ax12olem1  1927  ax12olem3  1929  ax10lem4  1941  ax11b  1995  sb6rf  2091  sb56  2098  exsb  2130  mo  2226  exmoeu  2246  morimv  2252  eupickbi  2270  2mo  2282  2eu1  2284  exists2  2294  r19.12  2728  2gencl  2889  3gencl  2890  rspccv  2953  ceqex  2970  mob  3019  euind  3024  reuind  3040  2rmorex  3041  sseq2  3294  reupick2  3542  uneqdifeq  3639  difsn  3846  eqsn  3868  iinss2  4019  sspwb  4119  pwadjoin  4120  preq12b  4128  iotaval  4351  nncaddccl  4420  nnsucelrlem2  4426  nndisjeq  4430  ltfintri  4467  ncfinraise  4482  ncfinlower  4484  tfin11  4494  tfinltfinlem1  4501  sucoddeven  4512  evenoddnnnul  4515  evenodddisj  4517  eventfin  4518  oddtfin  4519  sfindbl  4531  spfinsfincl  4540  vfinspsslem1  4551  vfinspss  4552  vfinspeqtncv  4554  phi11lem1  4596  copsexg  4608  2optocl  4840  3optocl  4841  xp11  5057  funmo  5126  fss  5231  fv3  5342  tz6.12c  5348  tz6.12i  5349  funfvima  5460  fvclss  5463  f1fveq  5474  isotr  5496  oprabid  5551  clos1conn  5880  2ecoptocl  5998  3ecoptocl  5999  enprmaplem3  6079  enprmaplem5  6081  nenpw1pwlem2  6086  leconnnc  6219  letc  6232  ce2le  6234  nclenn  6250  nchoicelem17  6306  nchoicelem19  6308  fnfreclem3  6320  fnfrec  6321