Theorem com12 13

Description: Inference that swaps (commutes) antecedents in an implication.

Hypothesis

Ref	Expression
comm.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
com12	⊢ (ψ → (φ → χ))

Proof of Theorem com12

Step	Hyp	Ref	Expression
1		ax-1 3	. 2 ⊢ (ψ → (φ → ψ))
2		comm.1	. . 3 ⊢ (φ → (ψ → χ))
3	2	a2i 8	. 2 ⊢ ((φ → ψ) → (φ → χ))
4	1, 3	syl 12	1 ⊢ (ψ → (φ → χ))

Syntax hints:   → wi 2

This theorem is referenced by:  a1d 14  syl2 17  pm2.27 30  com13 33  mpi 44  mpcom 49  sylcom 51  syli 52  syl9r 56  pm2.43b 61  pm2.24 72  pm2.61d2 111  pm2.61d 112  expt 123  biimpcd 137  biimprcd 138  dfor2 199  pm2.621 211  orel1 212  pm3.21 233  imdistanri 341  ibib 448  pm5.18 497  mtt 534  biantrud 545  ecase3d 560  dedlem0a 567  dedlem0b 568  3com12 614  meredith 644  hbimd 787  19.21g 792  eqt2 815  a4a 842  sbequ2 864  sbn2 881  sb5f1 917  cbval2 974  cbvex2 975  cbvald 977  mo 1020  mo2 1026  exmoeu 1039  moimv 1044  mopick 1054  2moswap 1064  2eu1 1067  2eu2 1068  r19.12 1281  r19.27av 1293  ceqsalg 1362  gencl 1365  2gencl 1366  3gencl 1367  cgsex2g 1368  cgsex4g 1369  vtocl2gf 1385  vtocl2ga 1388  vtocl3ga 1389  cla4e2gv 1398  ceqex 1410  mo2icl 1434  sseq2 1522  reuhyp 1581  minel 1743  r19.2z 1766  elsnc2g 1831  disjsn 1836  sspwb 1863  preq12b 1874  ssuni 1937  uniss2 1942  difex2 1951  reuuni1 1955  reuuni4 1959  unipw 1960  intmin 1982  iunpw 2040  pocl 2132  solin 2145  sotric 2148  sotrieq 2149  supub 2160  suplub 2161  supsn 2168  frss 2173  fr2nr 2177  fr3nr 2178  efrirr 2180  tz7.2 2183  dfwe2 2187  wefrc 2195  nordeq 2218  ordelord 2221  tz7.7 2224  ordtri1 2231  ordtri3 2234  onfr 2237  tfi 2244  ordtr2 2257  oneqmin 2273  nsuceq0 2306  trsuc 2308  onpwsuc 2315  ordsuc 2318  sucssel 2321  ordsucun 2333  suc11 2341  onssneli 2349  nlimsuc 2363  ordzsl 2366  ordom 2382  limom 2387  peano5 2394  2optocl 2470  3optocl 2471  opres 2580  resieq 2581  funssres 2698  funcnvuni 2706  fneu 2728  fnun 2730  fnex 2740  fun 2763  fornex 2793  fv3 2839  tz6.12-1 2842  tz6.12-2 2845  tz6.12c 2846  tz6.12i 2847  fvopab2 2878  cleqfv 2880  fsn 2895  funfvima 2904  funfvima3 2906  fvclss 2907  f1fveq 2918  isomin 2937  tfrlem8 2956  tfrlem9 2957  tfrlem10 2958  tfr3 2964  tz7.48-1 2994  tz7.48-2 2995  tz7.48-3 2996  tz7.49 2997  abianfp 3000  eloprabg 3035  oprabvalig 3048  ndmoprcl 3058  oacl 3138  omcl 3139  oecl 3140  oawordri 3152  oaordex 3160  oalimcl 3162  oaass 3163  omordi 3164  oen0 3165  nnacl 3172  nnmcl 3173  nnacom 3175  nnmordi 3188  nnmord 3189  omsmolem 3195  erth 3219  erdisj 3223  ectocl 3238  ecoptocl 3239  2ecoptocl 3240  3ecoptocl 3241  eceqopreq 3249  th3qlem2 3251  mapsn 3269  mapss 3270  eqeng 3296  dom2d 3307  xpdom2 3345  pw2en 3348  enen2 3376  domen2 3378  mapunen 3397  limensuc 3402  php 3409  php3 3411  onomeneq 3414  sucdomi 3419  pssinf 3422  isfinite1 3425  infsdomnn 3426  ssnn 3429  unblem2 3432  eirrv 3449  suc11reg 3456  inf0 3457  inf3lemd 3463  inf3lem1 3464  inf3lem2 3465  inf3lem3 3466  inf3lem5 3468  inf3lem6 3469  infensuc 3484  trcl 3489  zfregs 3491  tz9.12lem1 3503  rankr1 3518  rankel 3524  scottex 3541  aceq3lem 3555  aceq5 3563  ac6lem 3575  ac6s 3577  kmlem2 3581  kmlem4 3583  kmlem8 3587  kmlem11 3590  kmlem12 3591  numthlem 3598  weth 3602  zornlem3 3605  zornlem4 3606  zornlem5 3607  zornlem6 3608  zornlem7 3609  fodom 3613  imadomg 3616  cardnn 3631  carden 3638  sdomsdomcard 3654  ondomon 3662  ondomcard 3663  carduni 3664  alephordi 3679  alephsucdom 3685  cardaleph 3690  isinfcard 3692  iscard3 3693  axrepndlem2 3739  axrepnd 3740  axregndlem1 3748  axregndlem2 3749  axregnd 3750  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  addclpi 3814  addnidpi 3822  indpi 3828  ltexpq 3874  ltexpq2 3875  nsmallpq 3877  ltbtwnpq 3878  ltrpq 3879  genpnnp 3902  1pr 3911  distrlem4pr 3924  distrlem5pr 3925  prlem934 3933  ltaddpr2 3935  ltexprlem7 3942  ltexpri 3943  addcanpr 3946  prlem936b 3948  reclem2pr 3951  reclem3pr 3952  mulcmpblnr 3977  ssgt0sr 4011  map2psrpr 4014  suppsrlem 4015  supsrlem2 4020  suprelem 4053  negeu 4124  addsubt 4151  mul0or 4210  receu 4215  div23t 4240  ltmullem 4337  divgt0 4390  divge0 4392  nn1suc 4435  nnaddclt 4436  nnleltp1t 4448  nndiv 4453  sup3 4511  nnunb 4520  creui 4533  lt0nnn0 4549  nn0subt 4587  zltp1let 4597  uzwo 4605  nnwoOLD 4608  nn0ind 4612  uzwo3lem1 4614  uzwo3lem2 4615  qret 4631  om2uzlt 4654  om2uzran 4655  seqrn 4673  expcllem 4682  expaddt 4698  sqrlem18 4748  climunii 4883  ruclem33 4917  ruclem35 4919  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem10 4942  his6 5057  hial0 5058  hial2eqt 5060  hlimunii 5143  chsscm 5147  ocsh 5164  ocorth 5172  ocin 5177  occllem6 5185  projlem8 5200  projlem13 5205  projlem15 5207  projlem28 5220  projlem29 5221  pjthlem14 5238  dfch2 5254  pjoml 5271  shintcl 5294  chintcl 5296  shslej 5339  shlej1t 5356  shsidm 5358  shmods 5363  chnlen0 5369  h1dn0 5457  h1de2b 5459  h1de2ctlem 5460  h1de2ct 5461  spansn 5462  spansncol 5473  spansneleqi 5474  spansnss2t 5480  osumlem1 5530  osumlem4 5533  spansncv 5542  3oalem1 5552  pjrn 5587  pjss2co 5634  pjnormss 5638  pjorthco 5639  pjscj 5640  pjclem4a 5652  pj3lem1 5658  pj3cor1 5661  stle0 5680  stm1 5684  strlem3a 5693  strb 5699  cvnbtwnt 5718  spansncv2t 5725  mdbr2 5728  dmdbr 5731  atcveq0 5746  h1dat 5747  chcv1t 5751  chrelat2 5758  atcv0eq 5767  atcv1 5768  atcvat4 5775  mdsymlem3 5778  mdsymlem5 5780  mdsymlem6 5781  sumdmdlem 5786  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org