MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com13 Unicode version

Theorem com13 74
Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
com13  |-  ( ch 
->  ( ps  ->  ( ph  ->  th ) ) )

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3r 73 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com23 72 1  |-  ( ch 
->  ( ps  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com24  81  an13s  778  an31s  781  meredith  1394  peano5  4695  funopg  5302  abianfp  6487  omordi  6580  omeulem1  6596  brecop  6767  isinf  7092  fiint  7149  carduni  7630  dfac5  7771  dfac2  7773  cofsmo  7911  cfcoflem  7914  domtriomlem  8084  axdc3lem2  8093  nqereu  8569  squeeze0  9675  zmax  10329  xrsupsslem  10641  xrinfmsslem  10642  supxrunb1  10654  supxrunb2  10655  difreicc  10783  uzindi  11059  facwordi  11318  sqr2irr  12543  spwmo  14351  fbunfip  17580  grpomndo  21029  rngoueqz  21113  shmodsi  21984  kbass6  22717  mdsymlem6  23004  mdsymlem7  23005  cdj3lem2a  23032  cdj3lem3a  23035  predpo  24255  11st22nd  25148  prj1b  25182  prj3  25183  prl2  25272  domrancur1c  25305  dfps2  25392  reacomsmgrp2  25447  resgcom  25454  grpodlcan  25479  rngodmeqrn  25522  zerdivemp1  25539  rngoridfz  25540  svli2  25587  svs2  25590  cmptdst  25671  islimrs4  25685  bwt2  25695  iintlem1  25713  lvsovso2  25730  addcanrg  25770  cmpassoh  25904  ismonc  25917  cmpmon  25918  icmpmon  25919  isepic  25927  carinttar  26005  prismorcsetlemb  26016  clscnc  26113  pxysxy  26245  pdiveql  26271  zerdivemp1x  26689  psgnunilem4  27523  funressnfv  28096  funbrafv  28126  elfznelfzo  28213  injresinjlem  28214  injresinj  28215  nbgra0nb  28278  nbcusgra  28298  uvtxnbgra  28306  cusgrauvtx  28309  wlkdvspthlem  28365  cyclnspth  28376  fargshiftf1  28382  usgrcyclnl2  28387  nvnencycllem  28389  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  frgra3vlem1  28424  3cyclfrgrarn1  28435  3cyclfrgrarn  28436  4cycl2vnunb  28439  3imp31  28632  eel12131  28798  tratrbVD  28953  2uasbanhVD  29003  elpcliN  30704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator