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 489  anim12ii 557  pm2.76 573  ibib 588  pm2.26 657  pm5.18 658  bibif 679  mtt 710  ecase3d 752  dedlem0a 758  dedlem0b 759  3com12 835  3impd 845  3expd 848  mp3an1i 906  meredith 921  hbimd 1106  19.21t 1111  equtrr 1128  hbequid 1165  sbequ2 1175  equs5e 1194  ax11b 1215  sbn 1226  sb6rf 1255  sb56 1261  cbvald 1315  exmoeu 1406  moimv 1412  euor2 1430  2eu1 1442  r19.12 1732  r19.27av 1746  2gencl 1820  3gencl 1821  vtocl2ga 1844  vtocl3ga 1845  rcla4 1862  rcla4cv 1865  ceqex 1877  mo2icl 1914  sseq2 2073  uniiunlem 2122  disjsn 2431  eqsn 2465  preq12b 2474  intab 2550  dtruALT 2738  sspwb 2745  pocl 2835  solin 2848  sotrieq 2852  ralxfr 2889  iunpw 2904  frss 2911  fr2nr 2915  fr3nr 2916  efrirr 2918  tz7.7 2963  ordtri3 2973  ordtr2 2992  suc11 3083  onssneli 3091  ordom 3131  limom 3136  peano5 3143  2optocl 3226  3optocl 3227  relop 3265  xp11 3463  fornex 3664  fv3 3718  tz6.12-1 3721  tz6.12c 3725  tz6.12i 3726  fvopab2 3776  funfvima 3837  fvclss 3840  f1fveq 3861  isotr 3882  isotrALT 3883  isomin 3884  tfrlem2 3897  tfrlem9 3904  tfr3 3911  tz7.48-2 3942  tz7.48-3 3943  tz7.49 3944  abianfp 3947  oprabvalig 4009  oecl 4156  oaordex 4176  oalimcl 4178  oaass 4179  oarec 4180  omordi 4181  omlimcl 4193  odi 4194  oen0 4197  oewordri 4203  oeworde 4204  oaabs 4236  omsmolem 4240  erdisj 4270  2ecoptocl 4288  3ecoptocl 4289  eceqopreq 4297  th3qlem2 4299  xpdom2 4422  php 4493  onomeneq 4498  domfi 4516  unblem2 4518  unifi 4532  abfii4 4538  supub 4554  suplub 4555  supsnALT 4564  elirrv 4570  inf3lem1 4585  inf3lem2 4586  inf3lem3 4587  inf3lem5 4589  infensuc 4610  noinfep 4612  trcl 4617  rankr1 4646  rankel 4652  rankxpsuc 4687  scottex 4688  aceq3lem 4704  kmlem4 4740  kmlem9 4745  kmlem12 4748  kmlem13 4749  numthlem 4755  weth 4759  zorn2lem3 4762  zorn2lem4 4763  zorn2lem5 4764  zorn2lem6 4765  zorn2lem7 4766  ondomon 4828  cardaleph 4857  alephval2 4874  axrepnd 4918  indpi 5006  ltexpq 5052  ltexpq2 5053  nsmallpq 5055  ltbtwnpq 5056  ltrpq 5057  genpnnp 5080  1pr 5089  prlem934 5111  ltaddpr2 5113  ltexprlem7 5120  ltexpri 5121  prlem936b 5126  reclem2pr 5129  ssgt0sr 5189  suppsrlem 5193  suprelem 5231  addsubt 5356  mul0or 5663  squeeze0 5872  nnunb 6017  dfuz 6150  uzwo4OLD 6158  nn0ind-raph 6162  uzwo3lem1 6164  monoord 6231  seq1rn2 6258  icoshft 6341  uzwo 6387  uzwoOLD 6388  seqzrn2 6488  expcllem 6507  expeq0t 6517  expgt0t 6520  expgt1t 6523  mulexpt 6525  recexpt 6526  bernneq 6583  cjexpt 6752  absexpt 6803  abssubne0t 6820  cvg2 6859  facdivt 6879  bccl2t 6909  fsumrev 6967  2climnn 7039  2climnn0 7040  climaddlem3 7052  climmullem8 7063  iserzmulc1 7072  caucvglem6 7098  caucvg 7099  cvgratlem1 7185  cvgratlem2 7186  sin01bndlem2 7410  cos01bndlem2 7412  sin01gt0 7418  tgclt 7566  tgss2t 7579  subbas2 7587  indistop 7590  distop 7591  ssnei2 7671  cnpco 7708  cncnplem2 7714  meteq0 7751  opni3 7806  opnin 7809  neibl 7817  caun0 7880  metelcls 7900  xplmi 7907  lmcau 7930  bcthlem16 7948  bcthlem20 7952  bcthlem21 7953  bcthlem29 7961  ringid 8082  ipassi 8432  pslem 8573  spwmo 8580  efifolem5 8641  chsscm 9033  projlem28 9129  projlem29 9130  pjthlem14 9147  shintcl 9208  shmods 9277  spansn 9396  spansncol 9407  spansncv 9514  pjjs 9562  hoaddsubt 9659  eigorth 9680  homco2t 9817  lnopcon 9878  lnfncon 9905  cnlnadjlem5 9919  pjss2co 10003  pjnormss 10007  pj3cor1 10047  strb 10095  cvnbtwnt 10123  dmdmdt 10137  mdsl0 10145  csmdsym 10169  chrelat2 10200  cvat 10201  mdsymlem3 10240  mdsymlem6 10243  sumdmdlem2 10253  dmdbr5at 10255  uninqs 10342  infi1 10347  ficli 10368  fiiu2 10377  truni1 10386  mapdiscn 10398  mapudiscn 10399  cnvhmpha 10412  cnvhmphb 10413  hmphre 10417  hmeogrp 10425  homcard 10426  qusp 10430  filint 10437  fipfil2 10439  filintf 10443  fgsb 10444  efilcp 10445  filint2 10446  fisub 10447  infi 10448  fgsb2 10449  efilcp2 10450  cnfilca 10451  iintlem1 10476  iint 10478  cmppfd 10522  domcmpd 10523  codcmpd 10524  cmpasso 10550  cmpida 10551  cmpidb 10552  cmpassoh 10573  homgrf 10574  imonclem 10583  cmpmon 10585

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

Copyright terms: Public domain