HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem com12 26
Description: Inference that swaps (commutes) antecedents in an implication. (The proof was shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1 |- (ph -> (ps -> ch))
Assertion
Ref Expression
com12 |- (ps -> (ph -> ch))

Proof of Theorem com12
StepHypRef Expression
1 id 18 . 2 |- (ps -> ps)
2 com12.1 . 2 |- (ph -> (ps -> ch))
31, 2syl5com 25 1 |- (ps -> (ph -> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 4
This theorem is referenced by:  syl5 27  syl6com 30  mpcom 31  syli 32  pm2.27 34  pm2.43b 45  syl9r 66  com3r 72  pm2.86i 91  pm2.24 99  con3rr3 125  expt 145  jad 151  pm2.61 160  syl5ibcom 209  syl5ibrcom 211  biimprcdOLD 215  pm5.501 331  jaod 372  orel1 373  pm2.62 402  pm2.621OLD 405  impcom 422  imp3a 423  expcom 427  exp3a 428  pm3.21 435  imdistanri 676  pm2.64 739  pm2.75 800  ccased 900  dedlem0b 906  3impd 1146  3expd 1149  mp3an1i 1250  meredith 1266  simplbi2com 1346  a9wa9lem2 1453  a9wa9lem2OLD 1454  a9wa9lem6OLD 1459  hbimd 1553  19.21t 1556  equtrr 1573  sbequ2 1618  ax11b 1661  sb6rf 1703  sb56 1709  exmoeu 1871  moimv 1877  eupickbi 1895  2eu1 1909  exists2 1919  r19.12 2250  2gencl 2371  3gencl 2372  rcla4cv 2426  ceqex 2441  euind 2497  reuind 2508  sseq2 2685  uniiunlem 2737  uneqdifeq 2985  difsn 3167  eqsn 3182  preq12b 3191  intab 3280  iinss2 3333  trint0 3447  dtru 3516  sspwb 3535  copsexg 3560  pocl 3624  pofun 3633  solin 3641  frss 3657  fr2nr 3661  efrirr 3664  tz7.7 3708  ordtri3 3718  ordtr2 3726  suc11 3783  onssneli 3789  eusv2 3833  ralxfrALT 3859  iunpw 3880  fr3nr 3881  ordom 3971  peano5 3985  2optocl 4081  3optocl 4082  ssrel 4095  ssrelrel 4104  relop 4139  sotri3 4334  xp11 4364  relcnvtr 4426  fss 4569  fv3 4687  tz6.12-1 4690  tz6.12c 4694  tz6.12i 4695  fvco2 4733  fvopab2 4750  fornex 4800  funfvima 4855  fvclss 4859  f1fveq 4885  isotr 4910  isotrALT 4911  isomin 4912  oprabid 4943  ovg 5007  poxp 5256  soxp 5257  iotaval 5274  smores 5308  smoel 5316  smogt 5323  smoiso2 5325  smoge 5326  tfrlem2 5328  tfrlem9 5336  tfr3 5343  tz7.48-2 5372  tz7.48-3 5374  tz7.49 5375  abianfp 5378  oecl 5427  oaordex 5447  oalimcl 5449  oaass 5450  oarec 5451  omordi 5452  omlimcl 5464  odi 5465  omeulem1 5468  oen0 5471  oewordri 5477  oeworde 5478  oaabs 5514  omsmolem 5518  2ecoptocl 5585  3ecoptocl 5586  eceqoveq 5600  th3qlem2 5602  dom3d 5706  xpdom2 5750  infensuc 5872  php 5878  onomeneq 5883  unxpdomlem2 5897  unxpdomlem3 5898  isinf 5907  domfi 5916  findcard2 5924  unblem2 5935  unifi 5953  indexfi 5956  supub 5998  suplub 5999  supsnALT 6013  ordiso 6014  ordtypelem3 6017  ordtypelem4 6018  ordtypelem6 6020  ordtypelem7 6021  ordtype 6022  hartogs 6024  card2on 6027  card2inf 6028  elirrv 6034  inf3lem1 6052  inf3lem2 6053  inf3lem3 6054  inf3lem5 6056  noinfep 6080  noinfepOLD 6081  trcl 6082  tcel 6101  r1sdom 6112  rankr1c 6152  rankval3b 6155  rankr1 6163  rankel 6169  rankxpsuc 6209  scottex 6212  carddomi2 6252  ondomcard 6260  pr2ne 6275  dif1card 6277  aceq3lem 6308  aceq8clem 6323  fodomnum 6331  cardaleph 6336  cflim2 6407  cfsmolem 6413  domtriomlem 6426  axdc3lem4 6436  axdc4lem 6438  kmlem4 6470  kmlem9 6475  kmlem12 6478  kmlem13 6479  numthlem 6485  zorn2lem3 6492  zorn2lem4 6493  zorn2lem5 6494  zorn2lem6 6495  zorn2lem7 6496  zornn0 6500  axdclem 6501  axdclem2 6502  ondomon 6537  alephval2 6544  cfpwsdom 6571  axrepnd 6581  tsksdom 6632  tskr1om 6643  grupr 6673  gruiun 6675  ingru 6690  grothomex 6704  indpi 6784  nqereu 6807  genpnnp 6883  prlem934 6911  ltaddpr2 6913  reclem2pr 6926  mulgt0sr 6982  supsrlem 6988  mul0ori 7451  lemul1a 7588  squeeze0 7652  peano5nni 7701  nnunb 7865  fzind 7995  nn0ind-raph 7998  zindd 7999  eluzadd 8058  uzin 8061  iccss2 8330  icoshft 8362  fzen 8414  fzss1 8431  expcllem 8631  expeq0 8646  mulexp 8655  expword2i 8672  bernneq 8734  facdiv 8765  hashmap 8825  cjexp 8910  absexp 9040  abssubne0 9056  sin01gt0 9508  alzdvds 9614  dvdslegcd 9649  gcdneg 9658  rprimelpwr 9687  exprmfctlem 9734  prmpwdvds 9843  prmreclem4 9858  pslem 10170  spwmo 10181  gxnn0add 10671  gxnn0mul 10674  ismgm 10723  isexid2 10728  isga 10779  gagrpid 10787  gaass 10788  gapmlem 10790  rngodm1dm2 10843  rngosn4 10854  fiinopn 10884  tgcl 10929  tgss2 10943  distop 10954  ssnei2 11044  opnnei 11048  cnpnei 11101  cnpco 11104  cncnplem2 11110  cncmp 11137  cmpfi 11150  usinuniop 11155  dfcon2 11156  cnmptcom 11201  fbfinnfr 11230  isfildlem 11240  snfil 11248  fbunfip 11251  fgfild 11259  limfilss 11271  elfm2 11286  flimopn 11293  meteq0 11318  neibl 11389  reconn 11464  pi1gplem 11555  caubl 11613  ipassi 11952  ubthlem2 11983  minveclem5 11993  volsuplem 12159  cxpmul2 12788  qabvexp 12940  isch3 13283  shintcli 13371  shmodsi 13431  spansncvi 13712  pjjsi 13760  hoaddsub 13859  eigorthi 13880  homco2 14019  cnlnadjlem5 14113  pjss2coi 14206  pjnormssi 14210  pj3cor1i 14251  strb 14300  dmdmd 14342  mdsl0 14352  csmdsymi 14376  chrelat2i 14407  cvati 14408  mdsymlem3 14447  mdsymlem6 14450  sumdmdlem2 14461  dmdbr5ati 14464  3ccased 14632  dedekind 14638  dfres3 14676  dfon2lem3 14706  omssadd 14719  rdgprc 14728  trpredmintr 14815  trpredrec 14822  wfr3g 14836  wfrlem12 14848  frr3g 14861  frrlem11 14874  sltval2 14890  axfelem13 14939  elfuns 15041  axcontlem4 15179  cgrextend 15215  btwndiff 15234  btwnconn1lem12 15305  brsegle 15315  broutsideof2 15329  funray 15347  meran1 15509  waj-ax 15512  arg-ax 15514  wl-pm2.86i 15557  copsexgb 15597  evpexun 15625  cpref 15679  inttr 15684  isunscov 15686  restidsing 15690  twsymr 15692  prj1b 15693  prj3 15694  set2elt 15706  fixpc 15714  surjsec 15742  injrec2 15743  surjsec2 15744  elovdm2 15752  domintrefc 15753  mapmapmap 15778  injsurinj 15779  repfuntw 15791  repcpwti 15792  cbcpcp 15793  unprj 15798  prl 15799  prl2 15801  prjmapcp2 15802  dstr 15803  nZdef 15812  jidd 15824  midd 15825  preotr2 15859  int2pre 15861  ubpar 15887  inposet 15904  tolat 15915  pospos 15919  toplat 15922  latdir 15927  ridlideq 15969  rzrlzreq 15970  resgcom 15985  symgfo 16003  curgrpact 16008  grpodivone 16009  grpodivfo 16010  rltrran 16051  zerdivemp1 16073  zintdom 16075  muldisc 16117  svli2 16120  svs2 16123  truni1 16141  truni2 16142  truni3 16143  inttop2 16151  npmp 16157  mapdiscnlem 16164  mapdiscn 16165  mapudiscn 16166  nsn 16168  top2ind 16193  top2usne 16194  homindlem3 16196  intopcoaconlem3b 16197  intopcoaconc 16200  qusp 16201  intcont 16202  prtoptop 16208  prcnt 16210  efilcp 16211  fisub 16213  fbaslim2 16220  limfilnei 16227  conttnf 16228  iscnp3 16230  cnpfillim4 16231  cmptdst 16235  limhun 16237  exopcopn 16239  prdnei 16240  limptlimpr2lem1 16241  limptlimpr2lem2 16242  flimfnei2 16244  islimrs 16247  islimrs3 16248  islimrs4 16249  bwt2 16264  grpohmlem1 16289  grpohmlem2 16290  grpohmlem3 16291  grpohmlem4 16292  grpohmlem5 16293  grpohm 16294  iintlem1 16314  iint 16316  cnvtr 16320  mlteqer 16321  xrletr2 16322  lteqtpos 16327  lvsovso 16343  lvsovso3 16345  supnuf 16346  claddrvr 16365  sigadd 16366  addcomv 16372  addcanrg 16384  negveudr 16386  subclrvd 16391  distsava 16406  intvconlem1 16422  consuba 16425  hdrmp 16428  cmppfd 16470  domcmpd 16471  codcmpd 16472  cmpasso 16498  cmpida 16499  cmpidb 16500  dualalg 16509  dualded 16510  dualcat2 16511  cmpassoh 16528  homgrf 16529  imonclem 16540  cmpmon 16542  iepiclem 16550  isepic 16551  idfisf 16567  propsrc 16592  partarelt1 16618  inttaror 16622  inttarcar 16623  fnctartar 16629  fnctartar2 16630  prismorcset2 16641  morexcmp 16690  cmpmor 16698  setiscat 16702  lemindclsbu 16753  indcls2 16754  clscnc 16768  pgapspf2 16811  elicc3 16844  fictb 16849  finsschain 16850  nn0prpwlem 16857  nn0prpw 16858  qredeq 16859  2ndcctbss 16917  fnetr 16934  topbasfne 16938  fnessref 16942  neibastop1 16957  neibastop2lem2 16959  neibastop2lem3 16960  neibastop3 16963  topmtcl 16964  fnejoin1 16969  fnejoin2 16970  t0dist 16980  t1sep 16985  regsep 16989  nrmsep 16993  nrmsep2 16994  fmfnfmlem1 17035  flimfbas 17042  fclsfnflim 17055  fcluscomplem 17061  fzmul 17201  fdc 17215  seqpo 17217  incsequz 17218  heibor1lem 17278  ghomco 17320  zerdivemp1x 17333  pridlc 17443  ceqsex3OLD 17473  pm14.24 17606  sb5ALT 17704  truniALT 17721  onfrALTlem3 17725  ee223 17797  3orbi123VD 17945  sbc3orgVD 17946  exbirVD 17948  exbiriVD 17949  sbcim2gVD 17970  trsbcVD 17972  truniALTVD 17973  onfrALTlem3VD 17982  onfrALTlem2VD 17984  csbrngVD 17991  19.41rgVD 17997  a9e2eqVD 18002  a9e2ndeqVD 18004  2uasbanhVD 18006  sb5ALTVD 18007  vk15.4jVD 18008  cdleme18d 20764  tendovalco 21258  cdlemn11pre 21715  dihord2pre 21730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain