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.61d 125  pm2.61nii 129  pm2.6 131  expt 140  biimpcd 153  biimprcd 154  syl5cbi 207  syl5cbir 209  pm2.621 247  orel1 249  pm2.53 252  pm3.21 282  pm3.37 284  impcom 349  expcom 372  pm2.64 430  imdistanri 446  ancom1s 493  anim12ii 562  pm2.76 578  ibib 593  pm2.26 662  pm5.18 663  bibif 685  mtt 717  ecase3d 759  dedlem0a 765  dedlem0b 766  3com12 843  3impd 853  3expd 856  mp3an1i 915  meredith 931  hbimd 1146  19.21t 1151  equtrr 1169  sbequ2 1216  equs5e 1235  ax11b 1257  sbn 1268  sb6rf 1298  sb56 1304  cbvald 1358  exmoeu 1452  moimv 1458  euor2 1477  2eu1 1489  r19.12 1786  r19.27av 1800  2gencl 1875  3gencl 1876  vtocl2ga 1899  vtocl3ga 1900  rcla4 1917  rcla4cv 1920  ceqex 1932  mo2icl 1969  sseq2 2135  uniiunlem 2184  disjsn 2502  eqsn 2539  preq12b 2548  intab 2627  dtru 2831  sspwb 2835  pocl 2922  solin 2936  sotrieq 2940  frss 2951  fr2nr 2955  efrirr 2957  tz7.7 3001  ordtri3 3011  ordtr2 3019  suc11 3073  onssneli 3079  ralxfr 3122  iunpw 3137  fr3nr 3138  ordom 3228  limom 3233  peano5 3241  2optocl 3322  3optocl 3323  relop 3365  xp11 3561  fornex 3787  fv3 3844  tz6.12-1 3847  tz6.12c 3851  tz6.12i 3852  fvopab2 3902  funfvima 3966  fvclss 3969  f1fveq 3990  isotr 4011  isotrALT 4012  isomin 4013  oprabvalig 4084  tfrlem2 4213  tfrlem9 4220  tfr3 4227  tz7.48-2 4258  tz7.48-3 4259  tz7.49 4260  abianfp 4263  oecl 4308  oaordex 4328  oalimcl 4330  oaass 4331  oarec 4332  omordi 4333  omlimcl 4345  odi 4346  oen0 4349  oewordri 4355  oeworde 4356  oaabs 4392  omsmolem 4396  erdisj 4426  2ecoptocl 4445  3ecoptocl 4446  eceqopreq 4454  th3qlem2 4456  xpdom2 4583  ac6sfilem3 4590  ac6sfi 4591  php 4660  onomeneq 4665  domfi 4684  unblem2 4687  unifi 4701  abfii4 4707  supub 4723  suplub 4724  supsnALT 4735  elirrv 4741  inf3lem1 4758  inf3lem2 4759  inf3lem3 4760  inf3lem5 4762  infensuc 4784  noinfep 4786  trcl 4791  rankr1 4820  rankel 4826  rankxpsuc 4861  scottex 4862  aceq3lem 4878  kmlem4 4914  kmlem9 4919  kmlem12 4922  kmlem13 4923  numthlem 4929  weth 4933  zorn2lem3 4936  zorn2lem4 4937  zorn2lem5 4938  zorn2lem6 4939  zorn2lem7 4940  ondomon 5006  cardaleph 5035  alephval2 5052  axrepnd 5100  indpi 5188  ltexpq 5234  ltexpq2 5235  nsmallpq 5237  ltbtwnpq 5238  ltrpq 5239  genpnnp 5262  1pr 5271  prlem934 5293  ltaddpr2 5295  ltexprlem7 5302  ltexpri 5303  prlem936b 5308  reclem2pr 5311  ssgt0sr 5371  suppsrlem 5375  suprelem 5413  addsub 5538  mul0ori 5846  squeeze0 6069  nnunb 6238  dfuzi 6373  uzwo4OLD 6381  nn0ind-raph 6385  zindd 6386  uzwo3lem1 6388  monoord 6482  icoshft 6535  uzwo 6582  uzwoOLD 6583  fzen 6622  seq1rn2 6686  seqzrn2 6751  expcllem 6770  expeq0 6780  expgt0 6783  expgt1 6786  mulexp 6788  exprec 6789  exprecOLD 6790  bernneq 6849  bernneqOLD 6850  cjexp 7018  absexp 7070  abssubne0 7085  cvg2i 7125  facdiv 7145  bccl2 7174  fsumrev 7232  2climnn 7305  2climnn0 7306  climaddlem3 7319  climmullem8 7330  iserzmulc1 7339  caucvglem6 7365  caucvgi 7366  cvgratlem1 7455  cvgratlem2 7456  sin01bndlem2 7677  cos01bndlem2 7679  sin01gt0 7685  tgcl 7836  tgss2 7849  subbas2 7857  distop 7861  ssnei2 7940  cnpco 7979  cncnplem2 7985  meteq0 8022  opni3 8076  opnin 8079  neibl 8087  metequiv 8091  caun0 8156  metelcls 8176  xplmi 8184  lmcau 8207  bcthlem16 8225  bcthlem20 8229  bcthlem21 8230  bcthlem29 8238  gxnn0add 8330  gxnn0mul 8333  ringid 8386  vacnlem3 8584  vacnlem6 8587  ipassi 8757  pslem 8909  spwmo 8918  efifolem5 8998  chsscmi 9388  projlem28 9489  projlem29 9490  pjthlem14 9508  shintcli 9569  shmodsi 9638  spansni 9756  spansncvi 9875  pjjsi 9923  hoaddsub 10022  eigorthi 10043  homco2 10180  lnopconi 10242  lnfnconi 10269  cnlnadjlem5 10283  pjss2coi 10372  pjnormssi 10376  pj3cor1i 10418  strbi 10466  cvnbtwn 10494  dmdmd 10508  mdsl0 10518  csmdsymi 10542  chrelat2i 10573  cvati 10574  mdsymlem3 10614  mdsymlem6 10617  sumdmdlem2 10628  dmdbr5ati 10631  uninqs 10730  infi1 10735  ficli 10756  domintref 10767  twpar2 10773  cpref 10782  inttr 10787  mlteqer 10789  xrletr2 10790  isunscov 10796  restidsing 10805  twsymr 10808  prj1 10809  unpde2eg22 10826  set2elt 10827  jidd 10840  midd 10841  fiiu2 10852  infi 10854  inposet 10868  lteqtpos 10880  pospos 10882  tostos 10883  toplat 10884  ismgm 10897  isexid2 10901  ismnd2 10928  grpmnd 10933  rnplrnml0 10946  ununr 10955  on1el4 10963  zrdivrng 10969  truni1 10999  truni2 11000  truni3 11001  mapdiscn 11014  mapudiscn 11015  nsn 11017  cnvhmpha 11031  cnvhmphb 11032  hmphre 11036  hmeogrp 11044  homcard 11045  hmeobc 11048  top2ind 11050  top2usne 11051  homindlem3 11053  subtopsin2 11067  qusp 11068  filint 11075  fipfil2 11077  filintf 11081  fgsb 11082  efilcp 11083  filint2 11084  fisub 11085  fgsb2 11086  efilcp2 11087  cnfilca 11088  rcfpfillem3 11091  rcfpfillem4 11092  rcfpfillem6 11094  bwt2 11123  usinuniop 11128  altretop 11144  iintlem1 11155  iint 11157  cnvtr 11161  cmppfd 11199  domcmpd 11200  codcmpd 11201  cmpasso 11227  cmpida 11228  cmpidb 11229  cmpassoh 11256  homgrf 11257  imonclem 11268  cmpmon 11270  iepiclem 11278  isepic 11279  idfisf 11295  elicc3 11410  fiss 11419  elfiun 11421  fictb 11423  inficlALT 11424  finsschain 11425  ordiso 11426  ordtypelem3 11429  ordtypelem4 11430  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  omsubsdomlem2 11441  elomsubsd 11446  infenomsub 11450  opnnei 11469  cnpnei 11472  hscptsscld 11491  compfipin0 11493  cncomp 11494  dfcon2 11501  subtopmet 11506  reconn 11512  iccconn 11514  2ndcctbss 11539  fnetr 11556  topbasfne 11560  fnessref 11564  neibastop1 11579  neibastop2lem2 11581  neibastop2lem3 11582  neibastop3 11585  topmtcl 11586  fnejoin1 11591  fnejoin2 11592  t0dist 11602  t1sep 11607  regsep 11611  nrmsep 11615  nrmsep2 11616  fbssint 11626  filssufillem 11655  filufint 11659  flimopn 11679  limfilss 11682  elfilmap2 11691  flimfbas 11713  fclsfnflim 11726  fcluscomplem 11732  filnetlem5 11767  filnet 11768  isga 11772  ssga 11777  gagrpid 11780  gaass 11781  gapmlem 11783  ralun 11789  dif1en 11833  dif1card 11835  findcard 11836  fimax 11837  indexf 11847  inficl 11849  eluzadd 11860  sdclem1 11875  sdclem2 11876  sdc 11877  seqpo 11878  incsequz 11879  iccss2 11921  ismtyhmeolem 12006  heiborlem35 12045  heiborlem37 12047

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

Copyright terms: Public domain