Theorem com12 11

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

Hypothesis

Ref	Expression
com12.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
com12	|- (ps -> (ph -> ch))

Proof of Theorem com12

Step	Hyp	Ref	Expression
1		ax-1 4	. 2 |- (ps -> (ph -> ps))
2		com12.1	. . 3 |- (ph -> (ps -> ch))
3	2	a2i 9	. 2 |- ((ph -> ps) -> (ph -> ch))
4	1, 3	syl 10	1 |- (ps -> (ph -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim1 15  com13 33  mpcom 49  syl6com 53  syli 54  syl9r 58  pm2.27 62  pm2.43b 67  pm2.24 79  pm2.37OLD 99  pm2.61d 127  pm2.61nii 131  pm2.6 133  expt 142  biimpcd 155  biimprcd 156  syl5cbi 209  syl5cbir 211  pm2.621 249  orel1 251  pm2.53 254  pm3.21 284  pm3.37 286  impcom 351  expcom 374  pm2.64 429  imdistanri 444  ancom1s 490  anim12ii 558  pm2.76 574  ibib 589  pm2.26 658  pm5.18 659  bibif 680  mtt 711  ecase3d 753  dedlem0a 759  dedlem0b 760  3com12 836  3impd 846  3expd 849  mp3an1i 907  meredith 922  hbimd 1108  19.21t 1113  equtrr 1130  hbequid 1167  sbequ2 1177  equs5e 1196  ax11b 1218  sbn 1229  sb6rf 1258  sb56 1264  cbvald 1318  exmoeu 1411  moimv 1417  euor2 1435  2eu1 1447  r19.12 1737  r19.27av 1751  2gencl 1825  3gencl 1826  vtocl2ga 1849  vtocl3ga 1850  rcla4 1867  rcla4cv 1870  ceqex 1882  mo2icl 1919  sseq2 2079  uniiunlem 2128  disjsn 2437  eqsn 2470  preq12b 2479  intab 2555  dtruALT 2743  sspwb 2750  pocl 2839  solin 2852  sotrieq 2856  ralxfr 2894  iunpw 2909  frss 2916  fr2nr 2920  fr3nr 2921  efrirr 2923  tz7.7 2968  ordtri3 2978  ordtr2 2997  suc11 3088  onssneli 3096  ordom 3136  limom 3141  peano5 3148  2optocl 3231  3optocl 3232  relop 3270  xp11 3468  fornex 3670  fv3 3724  tz6.12-1 3727  tz6.12c 3731  tz6.12i 3732  fvopab2 3782  funfvima 3843  fvclss 3846  f1fveq 3867  isotr 3888  isotrALT 3889  isomin 3890  tfrlem2 3903  tfrlem9 3910  tfr3 3917  tz7.48-2 3948  tz7.48-3 3949  tz7.49 3950  abianfp 3953  oprabvalig 4015  oecl 4162  oaordex 4182  oalimcl 4184  oaass 4185  oarec 4186  omordi 4187  omlimcl 4199  odi 4200  oen0 4203  oewordri 4209  oeworde 4210  oaabs 4242  omsmolem 4246  erdisj 4276  2ecoptocl 4294  3ecoptocl 4295  eceqopreq 4303  th3qlem2 4305  xpdom2 4428  php 4499  onomeneq 4504  domfi 4522  unblem2 4524  unifi 4538  abfii4 4544  supub 4560  suplub 4561  supsnALT 4572  elirrv 4578  inf3lem1 4593  inf3lem2 4594  inf3lem3 4595  inf3lem5 4597  infensuc 4618  noinfep 4620  trcl 4625  rankr1 4654  rankel 4660  rankxpsuc 4695  scottex 4696  aceq3lem 4712  kmlem4 4748  kmlem9 4753  kmlem12 4756  kmlem13 4757  numthlem 4763  weth 4767  zorn2lem3 4770  zorn2lem4 4771  zorn2lem5 4772  zorn2lem6 4773  zorn2lem7 4774  ondomon 4836  cardaleph 4865  alephval2 4882  axrepnd 4926  indpi 5014  ltexpq 5060  ltexpq2 5061  nsmallpq 5063  ltbtwnpq 5064  ltrpq 5065  genpnnp 5088  1pr 5097  prlem934 5119  ltaddpr2 5121  ltexprlem7 5128  ltexpri 5129  prlem936b 5134  reclem2pr 5137  ssgt0sr 5197  suppsrlem 5201  suprelem 5239  addsubt 5364  mul0or 5671  squeeze0 5880  nnunb 6025  dfuz 6158  uzwo4OLD 6166  nn0ind-raph 6170  uzwo3lem1 6172  monoord 6239  seq1rn2 6266  icoshft 6349  uzwo 6395  uzwoOLD 6396  seqzrn2 6496  expcllem 6515  expeq0t 6525  expgt0t 6528  expgt1t 6531  mulexpt 6533  recexpt 6534  bernneq 6591  cjexpt 6760  absexpt 6811  abssubne0t 6828  cvg2 6867  facdivt 6887  bccl2t 6917  fsumrev 6975  2climnn 7047  2climnn0 7048  climaddlem3 7060  climmullem8 7071  iserzmulc1 7080  caucvglem6 7106  caucvg 7107  cvgratlem1 7193  cvgratlem2 7194  sin01bndlem2 7418  cos01bndlem2 7420  sin01gt0 7426  tgclt 7574  tgss2t 7587  subbas2 7595  indistop 7598  distop 7599  ssnei2 7680  cnpco 7719  cncnplem2 7725  meteq0 7762  opni3 7818  opnin 7821  neibl 7829  caun0 7896  metelcls 7916  xplmi 7923  lmcau 7946  bcthlem16 7964  bcthlem20 7968  bcthlem21 7969  bcthlem29 7977  ringid 8097  ipassi 8445  pslem 8590  spwmo 8598  efifolem5 8660  chsscm 9051  projlem28 9152  projlem29 9153  pjthlem14 9170  shintcl 9231  shmods 9300  spansn 9419  spansncol 9430  spansncv 9537  pjjs 9585  hoaddsubt 9682  eigorth 9703  homco2t 9840  lnopcon 9901  lnfncon 9928  cnlnadjlem5 9942  pjss2co 10030  pjnormss 10034  pj3cor1 10075  strb 10123  cvnbtwnt 10151  dmdmdt 10165  mdsl0 10174  csmdsym 10198  chrelat2 10229  cvat 10230  mdsymlem3 10269  mdsymlem6 10272  sumdmdlem2 10282  dmdbr5at 10284  uninqs 10378  infi1 10383  ficli 10404  fiiu2 10413  truni1 10422  mapdiscn 10434  mapudiscn 10435  cnvhmpha 10448  cnvhmphb 10449  hmphre 10453  hmeogrp 10461  homcard 10462  qusp 10466  filint 10473  fipfil2 10475  filintf 10479  fgsb 10480  efilcp 10481  filint2 10482  fisub 10483  infi 10484  fgsb2 10485  efilcp2 10486  cnfilca 10487  iintlem1 10512  iint 10514  cmppfd 10558  domcmpd 10559  codcmpd 10560  cmpasso 10586  cmpida 10587  cmpidb 10588  cmpassoh 10609  homgrf 10610  imonclem 10619  cmpmon 10621

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain