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 908  meredith 923  hbimd 1109  19.21t 1114  equtrr 1131  hbequid 1168  sbequ2 1178  equs5e 1197  ax11b 1219  sbn 1230  sb6rf 1259  sb56 1265  cbvald 1319  exmoeu 1412  moimv 1418  euor2 1436  2eu1 1448  r19.12 1738  r19.27av 1752  2gencl 1826  3gencl 1827  vtocl2ga 1850  vtocl3ga 1851  rcla4 1868  rcla4cv 1871  ceqex 1883  mo2icl 1920  sseq2 2080  uniiunlem 2129  disjsn 2438  eqsn 2471  preq12b 2480  intab 2556  dtruALT 2744  sspwb 2751  pocl 2840  solin 2853  sotrieq 2857  ralxfr 2895  iunpw 2910  frss 2917  fr2nr 2921  fr3nr 2922  efrirr 2924  tz7.7 2969  ordtri3 2979  ordtr2 2998  suc11 3089  onssneli 3097  ordom 3137  limom 3142  peano5 3149  2optocl 3232  3optocl 3233  relop 3271  xp11 3472  fornex 3674  fv3 3728  tz6.12-1 3731  tz6.12c 3735  tz6.12i 3736  fvopab2 3786  funfvima 3847  fvclss 3850  f1fveq 3871  isotr 3892  isotrALT 3893  isomin 3894  tfrlem2 3907  tfrlem9 3914  tfr3 3921  tz7.48-2 3952  tz7.48-3 3953  tz7.49 3954  abianfp 3957  oprabvalig 4019  oecl 4165  oaordex 4185  oalimcl 4187  oaass 4188  oarec 4189  omordi 4190  omlimcl 4202  odi 4203  oen0 4206  oewordri 4212  oeworde 4213  oaabs 4245  omsmolem 4249  erdisj 4279  2ecoptocl 4297  3ecoptocl 4298  eceqopreq 4306  th3qlem2 4308  xpdom2 4431  php 4502  onomeneq 4507  domfi 4525  unblem2 4527  unifi 4541  abfii4 4547  supub 4563  suplub 4564  supsnALT 4575  elirrv 4581  inf3lem1 4596  inf3lem2 4597  inf3lem3 4598  inf3lem5 4600  infensuc 4621  noinfep 4623  trcl 4628  rankr1 4657  rankel 4663  rankxpsuc 4698  scottex 4699  aceq3lem 4715  kmlem4 4751  kmlem9 4756  kmlem12 4759  kmlem13 4760  numthlem 4766  weth 4770  zorn2lem3 4773  zorn2lem4 4774  zorn2lem5 4775  zorn2lem6 4776  zorn2lem7 4777  ondomon 4839  cardaleph 4868  alephval2 4885  axrepnd 4929  indpi 5017  ltexpq 5063  ltexpq2 5064  nsmallpq 5066  ltbtwnpq 5067  ltrpq 5068  genpnnp 5091  1pr 5100  prlem934 5122  ltaddpr2 5124  ltexprlem7 5131  ltexpri 5132  prlem936b 5137  reclem2pr 5140  ssgt0sr 5200  suppsrlem 5204  suprelem 5242  addsubt 5367  mul0or 5673  squeeze0 5882  nnunb 6027  dfuz 6160  uzwo4OLD 6168  nn0ind-raph 6172  uzwo3lem1 6174  monoord 6244  seq1rn2 6271  icoshft 6354  uzwo 6400  uzwoOLD 6401  seqzrn2 6501  expcllem 6520  expeq0t 6530  expgt0t 6534  expgt1t 6537  mulexpt 6539  recexpt 6540  bernneq 6597  cjexpt 6767  absexpt 6818  abssubne0t 6835  cvg2 6874  facdivt 6894  bccl2t 6924  fsumrev 6982  2climnn 7055  2climnn0 7056  climaddlem3 7069  climmullem8 7080  iserzmulc1 7089  caucvglem6 7115  caucvg 7116  cvgratlem1 7202  cvgratlem2 7203  sin01bndlem2 7427  cos01bndlem2 7429  sin01gt0 7435  tgclt 7584  tgss2t 7597  subbas2 7605  indistop 7608  distop 7609  ssnei2 7690  cnpco 7729  cncnplem2 7735  meteq0 7772  opni3 7828  opnin 7831  neibl 7839  caun0 7907  metelcls 7927  xplmi 7935  lmcau 7958  bcthlem16 7976  bcthlem20 7980  bcthlem21 7981  bcthlem29 7989  ringid 8109  ipassi 8460  pslem 8605  spwmo 8613  efifolem5 8676  chsscm 9067  projlem28 9168  projlem29 9169  pjthlem14 9187  shintcl 9248  shmods 9317  spansn 9436  spansncol 9447  spansncv 9554  pjjs 9602  hoaddsubt 9699  eigorth 9720  homco2t 9858  lnopcon 9919  lnfncon 9946  cnlnadjlem5 9960  pjss2co 10048  pjnormss 10052  pj3cor1 10093  strb 10141  cvnbtwnt 10169  dmdmdt 10183  mdsl0 10193  csmdsym 10217  chrelat2 10248  cvat 10249  mdsymlem3 10288  mdsymlem6 10291  sumdmdlem2 10302  dmdbr5at 10305  uninqs 10400  infi1 10405  ficli 10426  fiiu2 10436  truni1 10445  mapdiscn 10457  mapudiscn 10458  cnvhmpha 10471  cnvhmphb 10472  hmphre 10476  hmeogrp 10484  homcard 10485  qusp 10489  filint 10496  fipfil2 10498  filintf 10502  fgsb 10503  efilcp 10504  filint2 10505  fisub 10506  infi 10507  fgsb2 10508  efilcp2 10509  cnfilca 10510  rcfpfillem2 10512  rcfpfillem3 10513  rcfpfillem4 10514  rcfpfillem6 10516  iintlem1 10548  iint 10550  cmppfd 10594  domcmpd 10595  codcmpd 10596  cmpasso 10622  cmpida 10623  cmpidb 10624  cmpassoh 10645  homgrf 10646  imonclem 10655  cmpmon 10657  idfisf 10670

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

Copyright terms: Public domain